mathlib docs: order.filter.lift

def filter.lift {α : Type u_1} {β : Type u_2} :

filter α → (set α → filter β) → filter β

A variant on bind using a function g taking a set instead of a member of α. This is essentially a push-forward along a function mapping each set to a filter.

Equations

f.lift g = ⨅ (s : set α) (H : s ∈ f), g s

source

theorem filter.has_basis.mem_lift_iff {α : Type u_1} {γ : Type u_3} {ι : Type u_2} {p : ι → Prop} {s : ι → set α} {f : filter α} (hf : f.has_basis p s) {β : ι → Type u_4} {pg : Π (i : ι), β i → Prop} {sg : Π (i : ι), β i → set γ} {g : set α → filter γ} (hg : ∀ (i : ι), (g (s i)).has_basis (pg i) (sg i)) (gm : monotone g) {s_1 : set γ} :

s_1 ∈ f.lift g ↔ ∃ (i : ι) (hi : p i) (x : β i) (hx : pg i x), sg i x ⊆ s_1

If (p : ι → Prop, s : ι → set α) is a basis of a filter f, g is a monotone function set α → filter γ, and for each i, (pg : β i → Prop, sg : β i → set α) is a basis of the filter g (s i), then (λ (i : ι) (x : β i), p i ∧ pg i x, λ (i : ι) (x : β i), sg i x) is a basis of the filter f.lift g.

This basis is parametrized by i : ι and x : β i, so in order to formulate this fact using has_basis one has to use Σ i, β i as the index type, see filter.has_basis.lift. This lemma states the corresponding mem_iff statement without using a sigma type.

source

theorem filter.has_basis.lift {α : Type u_1} {γ : Type u_3} {ι : Type u_2} {p : ι → Prop} {s : ι → set α} {f : filter α} (hf : f.has_basis p s) {β : ι → Type u_4} {pg : Π (i : ι), β i → Prop} {sg : Π (i : ι), β i → set γ} {g : set α → filter γ} :

(∀ (i : ι), (g (s i)).has_basis (pg i) (sg i)) → monotone g → (f.lift g).has_basis (λ (i : Σ (i : ι), β i), p i.fst ∧ pg i.fst i.snd) (λ (i : Σ (i : ι), β i), sg i.fst i.snd)

If (p : ι → Prop, s : ι → set α) is a basis of a filter f, g is a monotone function set α → filter γ, and for each i, (pg : β i → Prop, sg : β i → set α) is a basis of the filter g (s i), then (λ (i : ι) (x : β i), p i ∧ pg i x, λ (i : ι) (x : β i), sg i x) is a basis of the filter f.lift g.

This basis is parametrized by i : ι and x : β i, so in order to formulate this fact using has_basis one has to use Σ i, β i as the index type. See also filter.has_basis.mem_lift_iff for the corresponding mem_iff statement formulated without using a sigma type.

source

theorem filter.mem_lift_sets {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → filter β} (hg : monotone g) {s : set β} :

s ∈ f.lift g ↔ ∃ (t : set α) (H : t ∈ f), s ∈ g t

source

theorem filter.mem_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → filter β} {s : set β} {t : set α} :

t ∈ f → s ∈ g t → s ∈ f.lift g

source

theorem filter.lift_le {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → filter β} {h : filter β} {s : set α} :

s ∈ f → g s ≤ h → f.lift g ≤ h

source

theorem filter.le_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → filter β} {h : filter β} :

(∀ (s : set α), s ∈ f → h ≤ g s) → h ≤ f.lift g

source

theorem filter.lift_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : set α → filter β} :

f₁ ≤ f₂ → g₁ ≤ g₂ → f₁.lift g₁ ≤ f₂.lift g₂

source

theorem filter.lift_mono' {α : Type u_1} {β : Type u_2} {f : filter α} {g₁ g₂ : set α → filter β} :

(∀ (s : set α), s ∈ f → g₁ s ≤ g₂ s) → f.lift g₁ ≤ f.lift g₂

source

theorem filter.map_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α → filter β} {m : β → γ} :

monotone g → filter.map m (f.lift g) = f.lift (filter.map m ∘ g)

source

theorem filter.comap_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α → filter β} {m : γ → β} :

monotone g → filter.comap m (f.lift g) = f.lift (filter.comap m ∘ g)

source

theorem filter.comap_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {m : β → α} {g : set β → filter γ} :

monotone g → (filter.comap m f).lift g = f.lift (g ∘ set.preimage m)

source

theorem filter.map_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set β → filter γ} {m : α → β} :

monotone g → (filter.map m f).lift g = f.lift (g ∘ set.image m)

source

theorem filter.lift_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : filter β} {h : set α → set β → filter γ} :

f.lift (λ (s : set α), g.lift (h s)) = g.lift (λ (t : set β), f.lift (λ (s : set α), h s t))

source

theorem filter.lift_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α → filter β} {h : set β → filter γ} :

monotone g → (f.lift g).lift h = f.lift (λ (s : set α), (g s).lift h)

source

theorem filter.lift_lift_same_le_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → set α → filter β} :

f.lift (λ (s : set α), f.lift (g s)) ≤ f.lift (λ (s : set α), g s s)

source

theorem filter.lift_lift_same_eq_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → set α → filter β} :

(∀ (s : set α), monotone (λ (t : set α), g s t)) → (∀ (t : set α), monotone (λ (s : set α), g s t)) → f.lift (λ (s : set α), f.lift (g s)) = f.lift (λ (s : set α), g s s)

source

theorem filter.lift_principal {α : Type u_1} {β : Type u_2} {g : set α → filter β} {s : set α} :

monotone g → (filter.principal s).lift g = g s

source

theorem filter.monotone_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder γ] {f : γ → filter α} {g : γ → set α → filter β} :

monotone f → monotone g → monotone (λ (c : γ), (f c).lift (g c))

source

theorem filter.lift_ne_bot_iff {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → filter β} :

monotone g → ((f.lift g).ne_bot ↔ ∀ (s : set α), s ∈ f → (g s).ne_bot)

source

@[simp]

theorem filter.lift_const {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :

f.lift (λ (x : set α), g) = g

source

@[simp]

theorem filter.lift_inf {α : Type u_1} {β : Type u_2} {f : filter α} {g h : set α → filter β} :

f.lift (λ (x : set α), g x ⊓ h x) = f.lift g ⊓ f.lift h

source

@[simp]

theorem filter.lift_principal2 {α : Type u_1} {f : filter α} :

f.lift filter.principal = f

source

theorem filter.lift_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → filter α} {g : set α → filter β} [hι : nonempty ι] :

(∀ {s t : set α}, g s ⊓ g t = g (s ∩ t)) → ((infi f).lift g = ⨅ (i : ι), (f i).lift g)

source

def filter.lift' {α : Type u_1} {β : Type u_2} :

filter α → (set α → set β) → filter β

Specialize lift to functions set α → set β. This can be viewed as a generalization of map. This is essentially a push-forward along a function mapping each set to a set.

Equations

f.lift' h = f.lift (filter.principal ∘ h)

source

theorem filter.mem_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} {t : set α} :

t ∈ f → h t ∈ f.lift' h

source

theorem filter.has_basis.lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} {ι : Type u_3} {p : ι → Prop} {s : ι → set α} :

f.has_basis p s → monotone h → (f.lift' h).has_basis p (h ∘ s)

source

theorem filter.mem_lift'_sets {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} (hh : monotone h) {s : set β} :

s ∈ f.lift' h ↔ ∃ (t : set α) (H : t ∈ f), h t ⊆ s

source

theorem filter.eventually_lift'_iff {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} (hh : monotone h) {p : β → Prop} :

(∀ᶠ (y : β) in f.lift' h, p y) ↔ ∃ (t : set α) (H : t ∈ f), ∀ (y : β), y ∈ h t → p y

source

theorem filter.lift'_le {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → set β} {h : filter β} {s : set α} :

s ∈ f → filter.principal (g s) ≤ h → f.lift' g ≤ h

source

theorem filter.lift'_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {h₁ h₂ : set α → set β} :

f₁ ≤ f₂ → h₁ ≤ h₂ → f₁.lift' h₁ ≤ f₂.lift' h₂

source

theorem filter.lift'_mono' {α : Type u_1} {β : Type u_2} {f : filter α} {h₁ h₂ : set α → set β} :

(∀ (s : set α), s ∈ f → h₁ s ⊆ h₂ s) → f.lift' h₁ ≤ f.lift' h₂

source

theorem filter.lift'_cong {α : Type u_1} {β : Type u_2} {f : filter α} {h₁ h₂ : set α → set β} :

(∀ (s : set α), s ∈ f → h₁ s = h₂ s) → f.lift' h₁ = f.lift' h₂

source

theorem filter.map_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {h : set α → set β} {m : β → γ} :

monotone h → filter.map m (f.lift' h) = f.lift' (set.image m ∘ h)

source

theorem filter.map_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set β → set γ} {m : α → β} :

monotone g → (filter.map m f).lift' g = f.lift' (g ∘ set.image m)

source

theorem filter.comap_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {h : set α → set β} {m : γ → β} :

monotone h → filter.comap m (f.lift' h) = f.lift' (set.preimage m ∘ h)

source

theorem filter.comap_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {m : β → α} {g : set β → set γ} :

monotone g → (filter.comap m f).lift' g = f.lift' (g ∘ set.preimage m)

source

theorem filter.lift'_principal {α : Type u_1} {β : Type u_2} {h : set α → set β} {s : set α} :

monotone h → (filter.principal s).lift' h = filter.principal (h s)

source

theorem filter.lift'_pure {α : Type u_1} {β : Type u_2} {h : set α → set β} {a : α} :

monotone h → (has_pure.pure a).lift' h = filter.principal (h {a})

source

theorem filter.lift'_bot {α : Type u_1} {β : Type u_2} {h : set α → set β} :

monotone h → ⊥.lift' h = filter.principal (h ∅)

source

theorem filter.principal_le_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} {t : set β} :

(∀ (s : set α), s ∈ f → t ⊆ h s) → filter.principal t ≤ f.lift' h

source

theorem filter.monotone_lift' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder γ] {f : γ → filter α} {g : γ → set α → set β} :

monotone f → monotone g → monotone (λ (c : γ), (f c).lift' (g c))

source

theorem filter.lift_lift'_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α → set β} {h : set β → filter γ} :

monotone g → monotone h → (f.lift' g).lift h = f.lift (λ (s : set α), h (g s))

source

theorem filter.lift'_lift'_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α → set β} {h : set β → set γ} :

monotone g → monotone h → (f.lift' g).lift' h = f.lift' (λ (s : set α), h (g s))

source

theorem filter.lift'_lift_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α → filter β} {h : set β → set γ} :

monotone g → (f.lift g).lift' h = f.lift (λ (s : set α), (g s).lift' h)

source

theorem filter.lift_lift'_same_le_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → set α → set β} :

f.lift (λ (s : set α), f.lift' (g s)) ≤ f.lift' (λ (s : set α), g s s)

source

theorem filter.lift_lift'_same_eq_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α → set α → set β} :

(∀ (s : set α), monotone (λ (t : set α), g s t)) → (∀ (t : set α), monotone (λ (s : set α), g s t)) → f.lift (λ (s : set α), f.lift' (g s)) = f.lift' (λ (s : set α), g s s)

source

theorem filter.lift'_inf_principal_eq {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} {s : set β} :

f.lift' h ⊓ filter.principal s = f.lift' (λ (t : set α), h t ∩ s)

source

theorem filter.lift'_ne_bot_iff {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} :

monotone h → ((f.lift' h).ne_bot ↔ ∀ (s : set α), s ∈ f → (h s).nonempty)

source

@[simp]

theorem filter.lift'_id {α : Type u_1} {f : filter α} :

f.lift' id = f

source

theorem filter.le_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α → set β} {g : filter β} :

(∀ (s : set α), s ∈ f → h s ∈ g) → g ≤ f.lift' h

source

theorem filter.lift_infi' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → filter α} {g : set α → filter β} [nonempty ι] :

directed ge f → monotone g → ((infi f).lift g = ⨅ (i : ι), (f i).lift g)

source

theorem filter.lift'_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → filter α} {g : set α → set β} [nonempty ι] :

(∀ {s t : set α}, g s ∩ g t = g (s ∩ t)) → ((infi f).lift' g = ⨅ (i : ι), (f i).lift' g)

source

theorem filter.lift'_inf {α : Type u_1} {β : Type u_2} (f g : filter α) {s : set α → set β} :

(∀ {t₁ t₂ : set α}, s t₁ ∩ s t₂ = s (t₁ ∩ t₂)) → (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

source

theorem filter.comap_eq_lift' {α : Type u_1} {β : Type u_2} {f : filter β} {m : α → β} :

filter.comap m f = f.lift' (set.preimage m)

source

theorem filter.lift'_inf_powerset {α : Type u_1} (f g : filter α) :

(f ⊓ g).lift' set.powerset = f.lift' set.powerset ⊓ g.lift' set.powerset

source

theorem filter.eventually_lift'_powerset {α : Type u_1} {f : filter α} {p : set α → Prop} :

(∀ᶠ (s : set α) in f.lift' set.powerset, p s) ↔ ∃ (s : set α) (H : s ∈ f), ∀ (t : set α), t ⊆ s → p t

source

theorem filter.eventually_lift'_powerset' {α : Type u_1} {f : filter α} {p : set α → Prop} :

(∀ ⦃s t : set α⦄, s ⊆ t → p t → p s) → ((∀ᶠ (s : set α) in f.lift' set.powerset, p s) ↔ ∃ (s : set α) (H : s ∈ f), p s)

source

@[instance]

def filter.lift'_powerset_ne_bot {α : Type u_1} (f : filter α) :

(f.lift' set.powerset).ne_bot

Equations

_ = _

source

theorem filter.tendsto_lift'_powerset_mono {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {s t : α → set β} :

filter.tendsto t la (lb.lift' set.powerset) → (∀ᶠ (x : α) in la, s x ⊆ t x) → filter.tendsto s la (lb.lift' set.powerset)

source

@[simp]

theorem filter.eventually_lift'_powerset_forall {α : Type u_1} {f : filter α} {p : α → Prop} :

(∀ᶠ (s : set α) in f.lift' set.powerset, ∀ (x : α), x ∈ s → p x) ↔ ∀ᶠ (x : α) in f, p x

source

@[simp]

theorem filter.eventually_lift'_powerset_eventually {α : Type u_1} {f g : filter α} {p : α → Prop} :

(∀ᶠ (s : set α) in f.lift' set.powerset, ∀ᶠ (x : α) in g, x ∈ s → p x) ↔ ∀ᶠ (x : α) in f ⊓ g, p x

source

theorem filter.prod_def {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :

f.prod g = f.lift (λ (s : set α), g.lift' s.prod)

source

theorem filter.prod_same_eq {α : Type u_1} {f : filter α} :

f.prod f = f.lift' (λ (t : set α), t.prod t)

source

theorem filter.mem_prod_same_iff {α : Type u_1} {f : filter α} {s : set (α × α)} :

s ∈ f.prod f ↔ ∃ (t : set α) (H : t ∈ f), t.prod t ⊆ s

source

theorem filter.tendsto_prod_self_iff {α : Type u_1} {β : Type u_2} {f : α × α → β} {x : filter α} {y : filter β} :

filter.tendsto f (x.prod x) y ↔ ∀ (W : set β), W ∈ y → (∃ (U : set α) (H : U ∈ x), ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W)

source

theorem filter.prod_lift_lift {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {f₁ : filter α₁} {f₂ : filter α₂} {g₁ : set α₁ → filter β₁} {g₂ : set α₂ → filter β₂} :

monotone g₁ → monotone g₂ → (f₁.lift g₁).prod (f₂.lift g₂) = f₁.lift (λ (s : set α₁), f₂.lift (λ (t : set α₂), (g₁ s).prod (g₂ t)))

source

theorem filter.prod_lift'_lift' {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {f₁ : filter α₁} {f₂ : filter α₂} {g₁ : set α₁ → set β₁} {g₂ : set α₂ → set β₂} :

monotone g₁ → monotone g₂ → (f₁.lift' g₁).prod (f₂.lift' g₂) = f₁.lift (λ (s : set α₁), f₂.lift' (λ (t : set α₂), (g₁ s).prod (g₂ t)))

mathlib documentation

order.filter.lift

Lift filters along filter and set functions

General documentation

Additional documentation

Library

mathlib documentation

order.​filter.​lift

Lift filters along filter and set functions

General documentation

Additional documentation

Library

order.filter.lift