mathlib3 documentation

order.filter.lift

Lift filters along filter and set functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected]
def filter.lift {α : Type u_1} {β : Type u_2} (f : filter α) (g : set α 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
@[simp]
theorem filter.lift_top {α : Type u_1} {β : Type u_2} (g : set α filter β) :
theorem filter.has_basis.mem_lift_iff {α : Type u_1} {γ : Type u_3} {ι : Sort 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.

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 γ} (hg : (i : ι), (g (s i)).has_basis (pg i) (sg i)) (gm : 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.

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
theorem filter.sInter_lift_sets {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α filter β} (hg : monotone g) :
⋂₀ {s : set β | s f.lift g} = (s : set α) (H : s f), ⋂₀ {t : set β | t g s}
theorem filter.mem_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α filter β} {s : set β} {t : set α} (ht : t f) (hs : s g t) :
s f.lift g
theorem filter.lift_le {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α filter β} {h : filter β} {s : set α} (hs : s f) (hg : g s h) :
f.lift g h
theorem filter.le_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α filter β} {h : filter β} :
h f.lift g (s : set α), s f h g s
theorem filter.lift_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {g₁ g₂ : set α filter β} (hf : f₁ f₂) (hg : g₁ g₂) :
f₁.lift g₁ f₂.lift g₂
theorem filter.lift_mono' {α : Type u_1} {β : Type u_2} {f : filter α} {g₁ g₂ : set α filter β} (hg : (s : set α), s f g₁ s g₂ s) :
f.lift g₁ f.lift g₂
theorem filter.tendsto_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α filter β} {m : γ β} {l : filter γ} :
filter.tendsto m l (f.lift g) (s : set α), s f filter.tendsto m l (g s)
theorem filter.map_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α filter β} {m : β γ} (hg : monotone g) :
theorem filter.comap_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α filter β} {m : γ β} :
theorem filter.comap_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {m : β α} {g : set β filter γ} (hg : monotone g) :
theorem filter.lift_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set β filter γ} {m : α β} :
theorem filter.map_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set β filter γ} {m : α β} (hg : monotone g) :
(filter.map m f).lift g = f.lift (g set.image m)
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))
theorem filter.lift_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α filter β} {h : set β filter γ} (hg : monotone g) :
(f.lift g).lift h = f.lift (λ (s : set α), (g s).lift h)
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)
theorem filter.lift_lift_same_eq_lift {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α set α filter β} (hg₁ : (s : set α), monotone (λ (t : set α), g s t)) (hg₂ : (t : set α), monotone (λ (s : set α), g s t)) :
f.lift (λ (s : set α), f.lift (g s)) = f.lift (λ (s : set α), g s s)
theorem filter.lift_principal {α : Type u_1} {β : Type u_2} {g : set α filter β} {s : set α} (hg : monotone g) :
theorem filter.monotone_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder γ] {f : γ filter α} {g : γ set α filter β} (hf : monotone f) (hg : monotone g) :
monotone (λ (c : γ), (f c).lift (g c))
theorem filter.lift_ne_bot_iff {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α filter β} (hm : monotone g) :
(f.lift g).ne_bot (s : set α), s f (g s).ne_bot
@[simp]
theorem filter.lift_const {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.lift (λ (x : set α), g) = g
@[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
@[simp]
theorem filter.lift_principal2 {α : Type u_1} {f : filter α} :
theorem filter.lift_infi_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι filter α} {g : set α filter β} :
(infi f).lift g (i : ι), (f i).lift g
theorem filter.lift_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {f : ι filter α} {g : set α filter β} (hg : (s t : set α), g (s t) = g s g t) :
(infi f).lift g = (i : ι), (f i).lift g
theorem filter.lift_infi_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {f : ι filter α} {g : set α filter β} (hf : directed ge f) (hg : monotone g) :
(infi f).lift g = (i : ι), (f i).lift g
theorem filter.lift_infi_of_map_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι filter α} {g : set α filter β} (hg : (s t : set α), g (s t) = g s g t) (hg' : g set.univ = ) :
(infi f).lift g = (i : ι), (f i).lift g
@[protected]
def filter.lift' {α : Type u_1} {β : Type u_2} (f : filter α) (h : set α set β) :

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
@[simp]
theorem filter.lift'_top {α : Type u_1} {β : Type u_2} (h : set α set β) :
theorem filter.mem_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α set β} {t : set α} (ht : t f) :
h t f.lift' h
theorem filter.tendsto_lift' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {h : set α set β} {m : γ β} {l : filter γ} :
filter.tendsto m l (f.lift' h) (s : set α), s f (∀ᶠ (a : γ) in l, m a h s)
theorem filter.has_basis.lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α set β} {ι : Sort u_3} {p : ι Prop} {s : ι set α} (hf : f.has_basis p s) (hh : monotone h) :
(f.lift' h).has_basis p (h s)
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
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
theorem filter.sInter_lift'_sets {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α set β} (hh : monotone h) :
⋂₀ {s : set β | s f.lift' h} = (s : set α) (H : s f), h s
theorem filter.lift'_le {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α set β} {h : filter β} {s : set α} (hs : s f) (hg : filter.principal (g s) h) :
f.lift' g h
theorem filter.lift'_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : filter α} {h₁ h₂ : set α set β} (hf : f₁ f₂) (hh : h₁ h₂) :
f₁.lift' h₁ f₂.lift' h₂
theorem filter.lift'_mono' {α : Type u_1} {β : Type u_2} {f : filter α} {h₁ h₂ : set α set β} (hh : (s : set α), s f h₁ s h₂ s) :
f.lift' h₁ f.lift' h₂
theorem filter.lift'_cong {α : Type u_1} {β : Type u_2} {f : filter α} {h₁ h₂ : set α set β} (hh : (s : set α), s f h₁ s = h₂ s) :
f.lift' h₁ = f.lift' h₂
theorem filter.map_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {h : set α set β} {m : β γ} (hh : monotone h) :
theorem filter.lift'_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set β set γ} {m : α β} :
theorem filter.map_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set β set γ} {m : α β} (hg : monotone g) :
theorem filter.comap_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {h : set α set β} {m : γ β} :
theorem filter.comap_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {m : β α} {g : set β set γ} (hg : monotone g) :
theorem filter.lift'_principal {α : Type u_1} {β : Type u_2} {h : set α set β} {s : set α} (hh : monotone h) :
theorem filter.lift'_pure {α : Type u_1} {β : Type u_2} {h : set α set β} {a : α} (hh : monotone h) :
theorem filter.lift'_bot {α : Type u_1} {β : Type u_2} {h : set α set β} (hh : monotone h) :
theorem filter.le_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α set β} {g : filter β} :
g f.lift' h (s : set α), s f h s g
theorem filter.principal_le_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α set β} {t : set β} :
filter.principal t f.lift' h (s : set α), s f t h s
theorem filter.monotone_lift' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder γ] {f : γ filter α} {g : γ set α set β} (hf : monotone f) (hg : monotone g) :
monotone (λ (c : γ), (f c).lift' (g c))
theorem filter.lift_lift'_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α set β} {h : set β filter γ} (hg : monotone g) (hh : monotone h) :
(f.lift' g).lift h = f.lift (λ (s : set α), h (g s))
theorem filter.lift'_lift'_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α set β} {h : set β set γ} (hg : monotone g) (hh : monotone h) :
(f.lift' g).lift' h = f.lift' (λ (s : set α), h (g s))
theorem filter.lift'_lift_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {g : set α filter β} {h : set β set γ} (hg : monotone g) :
(f.lift g).lift' h = f.lift (λ (s : set α), (g s).lift' h)
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)
theorem filter.lift_lift'_same_eq_lift' {α : Type u_1} {β : Type u_2} {f : filter α} {g : set α set α set β} (hg₁ : (s : set α), monotone (λ (t : set α), g s t)) (hg₂ : (t : set α), monotone (λ (s : set α), g s t)) :
f.lift (λ (s : set α), f.lift' (g s)) = f.lift' (λ (s : set α), g s s)
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)
theorem filter.lift'_ne_bot_iff {α : Type u_1} {β : Type u_2} {f : filter α} {h : set α set β} (hh : monotone h) :
(f.lift' h).ne_bot (s : set α), s f (h s).nonempty
@[simp]
theorem filter.lift'_id {α : Type u_1} {f : filter α} :
f.lift' id = f
theorem filter.lift'_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {f : ι filter α} {g : set α set β} (hg : (s t : set α), g (s t) = g s g t) :
(infi f).lift' g = (i : ι), (f i).lift' g
theorem filter.lift'_infi_of_map_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι filter α} {g : set α set β} (hg : {s t : set α}, g (s t) = g s g t) (hg' : g set.univ = set.univ) :
(infi f).lift' g = (i : ι), (f i).lift' g
theorem filter.lift'_inf {α : Type u_1} {β : Type u_2} (f g : filter α) {s : set α set β} (hs : (t₁ t₂ : set α), s (t₁ t₂) = s t₁ s t₂) :
(f g).lift' s = f.lift' s g.lift' s
theorem filter.lift'_inf_le {α : Type u_1} {β : Type u_2} (f g : filter α) (s : set α set β) :
(f g).lift' s f.lift' s g.lift' s
theorem filter.comap_eq_lift' {α : Type u_1} {β : Type u_2} {f : filter β} {m : α β} :
theorem filter.prod_def {α : Type u_1} {β : Type u_2} {f : filter α} {g : filter β} :
f.prod g = f.lift (λ (s : set α), g.lift' (λ (t : set β), s ×ˢ t))
theorem filter.prod_same_eq {α : Type u_1} {f : filter α} :
f.prod f = f.lift' (λ (t : set α), t ×ˢ t)
theorem filter.mem_prod_same_iff {α : Type u_1} {f : filter α} {s : set × α)} :
s f.prod f (t : set α) (H : t f), t ×ˢ t s
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)
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 β₂} (hg₁ : monotone g₁) (hg₂ : monotone g₂) :
(f₁.lift g₁).prod (f₂.lift g₂) = f₁.lift (λ (s : set α₁), f₂.lift (λ (t : set α₂), (g₁ s).prod (g₂ t)))
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 β₂} (hg₁ : monotone g₁) (hg₂ : monotone g₂) :
(f₁.lift' g₁).prod (f₂.lift' g₂) = f₁.lift (λ (s : set α₁), f₂.lift' (λ (t : set α₂), g₁ s ×ˢ g₂ t))