# Lift filters along filter and set functions #

def Filter.lift {α : Type u_1} {β : Type u_2} (f : ) (g : Set α) :

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 = sf, g s
Instances For
@[simp]
theorem Filter.lift_top {α : Type u_1} {β : Type u_2} (g : Set α) :
.lift g = g Set.univ
theorem Filter.HasBasis.mem_lift_iff {α : Type u_1} {γ : Type u_3} {ι : Sort u_6} {p : ιProp} {s : ιSet α} {f : } (hf : f.HasBasis p s✝) {β : ιType u_5} {pg : (i : ι) → β iProp} {sg : (i : ι) → β iSet γ} {g : Set α} (hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)) (gm : ) {s : Set γ} :
s f.lift g ∃ (i : ι), p i ∃ (x : β i), pg i x sg i x s

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 (fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (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 Filter.HasBasis one has to use Σ i, β i as the index type, see Filter.HasBasis.lift. This lemma states the corresponding mem_iff statement without using a sigma type.

theorem Filter.HasBasis.lift {α : Type u_1} {γ : Type u_3} {ι : Type u_6} {p : ιProp} {s : ιSet α} {f : } (hf : f.HasBasis p s) {β : ιType u_5} {pg : (i : ι) → β iProp} {sg : (i : ι) → β iSet γ} {g : Set α} (hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)) (gm : ) :
(f.lift g).HasBasis (fun (i : (i : ι) × β i) => p i.fst pg i.fst i.snd) fun (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 (fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (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.HasBasis.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 : } {g : Set α} (hg : ) {s : Set β} :
s f.lift g tf, s g t
theorem Filter.sInter_lift_sets {α : Type u_1} {β : Type u_2} {f : } {g : Set α} (hg : ) :
⋂₀ {s : Set β | s f.lift g} = sf, ⋂₀ {t : Set β | t g s}
theorem Filter.mem_lift {α : Type u_1} {β : Type u_2} {f : } {g : Set α} {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 : } {g : Set α} {h : } {s : Set α} (hs : s f) (hg : g s h) :
f.lift g h
theorem Filter.le_lift {α : Type u_1} {β : Type u_2} {f : } {g : Set α} {h : } :
h f.lift g sf, h g s
theorem Filter.lift_mono {α : Type u_1} {β : Type u_2} {f₁ : } {f₂ : } {g₁ : Set α} {g₂ : Set α} (hf : f₁ f₂) (hg : g₁ g₂) :
f₁.lift g₁ f₂.lift g₂
theorem Filter.lift_mono' {α : Type u_1} {β : Type u_2} {f : } {g₁ : Set α} {g₂ : Set α} (hg : sf, g₁ s g₂ s) :
f.lift g₁ f.lift g₂
theorem Filter.tendsto_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set α} {m : γβ} {l : } :
Filter.Tendsto m l (f.lift g) sf, Filter.Tendsto m l (g s)
theorem Filter.map_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set α} {m : βγ} (hg : ) :
Filter.map m (f.lift g) = f.lift ( g)
theorem Filter.comap_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set α} {m : γβ} :
Filter.comap m (f.lift g) = f.lift ( g)
theorem Filter.comap_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {m : βα} {g : Set β} (hg : ) :
(Filter.comap m f).lift g = f.lift (g )
theorem Filter.lift_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set β} {m : αβ} :
(Filter.map m f).lift g f.lift (g )
theorem Filter.map_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set β} {m : αβ} (hg : ) :
(Filter.map m f).lift g = f.lift (g )
theorem Filter.lift_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : } {h : Set αSet β} :
(f.lift fun (s : Set α) => g.lift (h s)) = g.lift fun (t : Set β) => f.lift fun (s : Set α) => h s t
theorem Filter.lift_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set α} {h : Set β} (hg : ) :
(f.lift g).lift h = f.lift fun (s : Set α) => (g s).lift h
theorem Filter.lift_lift_same_le_lift {α : Type u_1} {β : Type u_2} {f : } {g : Set αSet α} :
(f.lift fun (s : Set α) => f.lift (g s)) f.lift fun (s : Set α) => g s s
theorem Filter.lift_lift_same_eq_lift {α : Type u_1} {β : Type u_2} {f : } {g : Set αSet α} (hg₁ : ∀ (s : Set α), Monotone fun (t : Set α) => g s t) (hg₂ : ∀ (t : Set α), Monotone fun (s : Set α) => g s t) :
(f.lift fun (s : Set α) => f.lift (g s)) = f.lift fun (s : Set α) => g s s
theorem Filter.lift_principal {α : Type u_1} {β : Type u_2} {g : Set α} {s : Set α} (hg : ) :
.lift g = g s
theorem Filter.monotone_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {f : γ} {g : γSet α} (hf : ) (hg : ) :
Monotone fun (c : γ) => (f c).lift (g c)
theorem Filter.lift_neBot_iff {α : Type u_1} {β : Type u_2} {f : } {g : Set α} (hm : ) :
(f.lift g).NeBot sf, (g s).NeBot
@[simp]
theorem Filter.lift_const {α : Type u_1} {β : Type u_2} {f : } {g : } :
(f.lift fun (x : Set α) => g) = g
@[simp]
theorem Filter.lift_inf {α : Type u_1} {β : Type u_2} {f : } {g : Set α} {h : Set α} :
(f.lift fun (x : Set α) => g x h x) = f.lift g f.lift h
@[simp]
theorem Filter.lift_principal2 {α : Type u_1} {f : } :
f.lift Filter.principal = f
theorem Filter.lift_iInf_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι} {g : Set α} :
(iInf f).lift g ⨅ (i : ι), (f i).lift g
theorem Filter.lift_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {f : ι} {g : Set α} (hg : ∀ (s t : Set α), g (s t) = g s g t) :
(iInf f).lift g = ⨅ (i : ι), (f i).lift g
theorem Filter.lift_iInf_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {f : ι} {g : Set α} (hf : Directed (fun (x1 x2 : ) => x1 x2) f) (hg : ) :
(iInf f).lift g = ⨅ (i : ι), (f i).lift g
theorem Filter.lift_iInf_of_map_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι} {g : Set α} (hg : ∀ (s t : Set α), g (s t) = g s g t) (hg' : g Set.univ = ) :
(iInf f).lift g = ⨅ (i : ι), (f i).lift g
def Filter.lift' {α : Type u_1} {β : Type u_2} (f : ) (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
• f.lift' h = f.lift (Filter.principal h)
Instances For
@[simp]
theorem Filter.lift'_top {α : Type u_1} {β : Type u_2} (h : Set αSet β) :
.lift' h = Filter.principal (h Set.univ)
theorem Filter.mem_lift' {α : Type u_1} {β : Type u_2} {f : } {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 : } {h : Set αSet β} {m : γβ} {l : } :
Filter.Tendsto m l (f.lift' h) sf, ∀ᶠ (a : γ) in l, m a h s
theorem Filter.HasBasis.lift' {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} {ι : Sort u_5} {p : ιProp} {s : ιSet α} (hf : f.HasBasis p s) (hh : ) :
(f.lift' h).HasBasis p (h s)
theorem Filter.mem_lift'_sets {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} (hh : ) {s : Set β} :
s f.lift' h tf, h t s
theorem Filter.eventually_lift'_iff {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} (hh : ) {p : βProp} :
(∀ᶠ (y : β) in f.lift' h, p y) tf, yh t, p y
theorem Filter.sInter_lift'_sets {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} (hh : ) :
⋂₀ {s : Set β | s f.lift' h} = sf, h s
theorem Filter.lift'_le {α : Type u_1} {β : Type u_2} {f : } {g : Set αSet β} {h : } {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₂ : } {h₁ : Set αSet β} {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 : } {h₁ : Set αSet β} {h₂ : Set αSet β} (hh : sf, h₁ s h₂ s) :
f.lift' h₁ f.lift' h₂
theorem Filter.lift'_cong {α : Type u_1} {β : Type u_2} {f : } {h₁ : Set αSet β} {h₂ : Set αSet β} (hh : sf, 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 : } {h : Set αSet β} {m : βγ} (hh : ) :
Filter.map m (f.lift' h) = f.lift' ( h)
theorem Filter.lift'_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set βSet γ} {m : αβ} :
(Filter.map m f).lift' g f.lift' (g )
theorem Filter.map_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set βSet γ} {m : αβ} (hg : ) :
(Filter.map m f).lift' g = f.lift' (g )
theorem Filter.comap_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {h : Set αSet β} {m : γβ} :
Filter.comap m (f.lift' h) = f.lift' ( h)
theorem Filter.comap_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {m : βα} {g : Set βSet γ} (hg : ) :
(Filter.comap m f).lift' g = f.lift' (g )
theorem Filter.lift'_principal {α : Type u_1} {β : Type u_2} {h : Set αSet β} {s : Set α} (hh : ) :
.lift' h = Filter.principal (h s)
theorem Filter.lift'_pure {α : Type u_1} {β : Type u_2} {h : Set αSet β} {a : α} (hh : ) :
(pure a).lift' h = Filter.principal (h {a})
theorem Filter.lift'_bot {α : Type u_1} {β : Type u_2} {h : Set αSet β} (hh : ) :
.lift' h =
theorem Filter.le_lift' {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} {g : } :
g f.lift' h sf, h s g
theorem Filter.principal_le_lift' {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} {t : Set β} :
f.lift' h sf, t h s
theorem Filter.monotone_lift' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {f : γ} {g : γSet αSet β} (hf : ) (hg : ) :
Monotone fun (c : γ) => (f c).lift' (g c)
theorem Filter.lift_lift'_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set αSet β} {h : Set β} (hg : ) (hh : ) :
(f.lift' g).lift h = f.lift fun (s : Set α) => h (g s)
theorem Filter.lift'_lift'_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set αSet β} {h : Set βSet γ} (hg : ) (hh : ) :
(f.lift' g).lift' h = f.lift' fun (s : Set α) => h (g s)
theorem Filter.lift'_lift_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {g : Set α} {h : Set βSet γ} (hg : ) :
(f.lift g).lift' h = f.lift fun (s : Set α) => (g s).lift' h
theorem Filter.lift_lift'_same_le_lift' {α : Type u_1} {β : Type u_2} {f : } {g : Set αSet αSet β} :
(f.lift fun (s : Set α) => f.lift' (g s)) f.lift' fun (s : Set α) => g s s
theorem Filter.lift_lift'_same_eq_lift' {α : Type u_1} {β : Type u_2} {f : } {g : Set αSet αSet β} (hg₁ : ∀ (s : Set α), Monotone fun (t : Set α) => g s t) (hg₂ : ∀ (t : Set α), Monotone fun (s : Set α) => g s t) :
(f.lift fun (s : Set α) => f.lift' (g s)) = f.lift' fun (s : Set α) => g s s
theorem Filter.lift'_inf_principal_eq {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} {s : Set β} :
f.lift' h = f.lift' fun (t : Set α) => h t s
theorem Filter.lift'_neBot_iff {α : Type u_1} {β : Type u_2} {f : } {h : Set αSet β} (hh : ) :
(f.lift' h).NeBot sf, (h s).Nonempty
@[simp]
theorem Filter.lift'_id {α : Type u_1} {f : } :
f.lift' id = f
theorem Filter.lift'_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {f : ι} {g : Set αSet β} (hg : ∀ (s t : Set α), g (s t) = g s g t) :
(iInf f).lift' g = ⨅ (i : ι), (f i).lift' g
theorem Filter.lift'_iInf_of_map_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι} {g : Set αSet β} (hg : ∀ {s t : Set α}, g (s t) = g s g t) (hg' : g Set.univ = Set.univ) :
(iInf f).lift' g = ⨅ (i : ι), (f i).lift' g
theorem Filter.lift'_inf {α : Type u_1} {β : Type u_2} (f : ) (g : ) {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 : ) (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 : } {m : αβ} :
= f.lift' (Set.preimage m)
theorem Filter.prod_def {α : Type u_1} {β : Type u_2} {f : } {g : } :
f ×ˢ g = f.lift fun (s : Set α) => g.lift' fun (t : Set β) => s ×ˢ t
theorem Filter.mem_prod_same_iff {α : Type u_1} {la : } {s : Set (α × α)} :
s la ×ˢ la tla, t ×ˢ t s

Alias of Filter.mem_prod_self_iff.

theorem Filter.prod_same_eq {α : Type u_1} {f : } :
f ×ˢ f = f.lift' fun (t : Set α) => t ×ˢ t
theorem Filter.tendsto_prod_self_iff {α : Type u_1} {β : Type u_2} {f : α × αβ} {x : } {y : } :
Filter.Tendsto f (x ×ˢ x) y Wy, Ux, ∀ (x x' : α), x Ux' Uf (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₁ ×ˢ f₂.lift g₂ = f₁.lift fun (s : Set α₁) => f₂.lift fun (t : Set α₂) => g₁ s ×ˢ 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₁ ×ˢ f₂.lift' g₂ = f₁.lift fun (s : Set α₁) => f₂.lift' fun (t : Set α₂) => g₁ s ×ˢ g₂ t