Documentation

Mathlib.Order.Filter.Lift

Lift filters along filter and set functions #

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 β) :
Filter.lift g = g Set.univ
theorem Filter.HasBasis.mem_lift_iff {α : Type u_2} {γ : Type u_4} {ι : Sort u_1} {p : ιProp} {s : ιSet α} {f : Filter α} (hf : Filter.HasBasis f p s) {β : ιType u_3} {pg : (i : ι) → β iProp} {sg : (i : ι) → β iSet γ} {g : Set αFilter γ} (hg : ∀ (i : ι), Filter.HasBasis (g (s i)) (pg i) (sg i)) (gm : Monotone g) {s : Set γ} :
s Filter.lift f g i, p i x, 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 (λ (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 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_2} {γ : Type u_4} {ι : Type u_1} {p : ιProp} {s : ιSet α} {f : Filter α} (hf : Filter.HasBasis f p s) {β : ιType u_3} {pg : (i : ι) → β iProp} {sg : (i : ι) → β iSet γ} {g : Set αFilter γ} (hg : ∀ (i : ι), Filter.HasBasis (g (s i)) (pg i) (sg i)) (gm : Monotone g) :
Filter.HasBasis (Filter.lift f g) (fun i => p i.fst pg i.fst i.snd) fun 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.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 : Filter α} {g : Set αFilter β} (hg : Monotone g) {s : Set β} :
s Filter.lift f g t, t f s g t
theorem Filter.interₛ_lift_sets {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set αFilter β} (hg : Monotone g) :
⋂₀ { s | s Filter.lift f g } = Set.interᵢ fun s => Set.interᵢ fun h => ⋂₀ { t | t g s }
theorem Filter.mem_lift {α : Type u_2} {β : Type u_1} {f : Filter α} {g : Set αFilter β} {s : Set β} {t : Set α} (ht : t f) (hs : s g t) :
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) :
theorem Filter.le_lift {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set αFilter β} {h : Filter β} :
h Filter.lift f g ∀ (s : Set α), s fh g s
theorem Filter.lift_mono {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {g₁ : Set αFilter β} {g₂ : Set αFilter β} (hf : f₁ f₂) (hg : g₁ g₂) :
Filter.lift f₁ g₁ Filter.lift f₂ g₂
theorem Filter.lift_mono' {α : Type u_1} {β : Type u_2} {f : Filter α} {g₁ : Set αFilter β} {g₂ : Set αFilter β} (hg : ∀ (s : Set α), s fg₁ s g₂ s) :
theorem Filter.tendsto_lift {α : Type u_3} {β : Type u_2} {γ : Type u_1} {f : Filter α} {g : Set αFilter β} {m : γβ} {l : Filter γ} :
Filter.Tendsto m l (Filter.lift f g) ∀ (s : Set α), s fFilter.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_3} {β : Type u_2} {γ : Type u_1} {f : Filter α} {g : Set αFilter β} {m : γβ} :
theorem Filter.comap_lift_eq2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : Filter α} {m : βα} {g : Set βFilter γ} (hg : Monotone g) :
theorem Filter.lift_map_le {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : Filter α} {g : Set βFilter γ} {m : αβ} :
theorem Filter.map_lift_eq2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : Filter α} {g : Set βFilter γ} {m : αβ} (hg : Monotone g) :
theorem Filter.lift_comm {α : Type u_2} {β : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Set αSet βFilter γ} :
(Filter.lift f fun s => Filter.lift g (h s)) = Filter.lift g fun t => Filter.lift f fun s => h s t
theorem Filter.lift_assoc {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : Filter α} {g : Set αFilter β} {h : Set βFilter γ} (hg : Monotone g) :
Filter.lift (Filter.lift f g) h = Filter.lift f fun s => Filter.lift (g s) h
theorem Filter.lift_lift_same_le_lift {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set αSet αFilter β} :
(Filter.lift f fun s => Filter.lift f (g s)) Filter.lift f fun s => 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 fun t => g s t) (hg₂ : ∀ (t : Set α), Monotone fun s => g s t) :
(Filter.lift f fun s => Filter.lift f (g s)) = Filter.lift f fun s => 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_2} {β : Type u_3} {γ : Type u_1} [inst : Preorder γ] {f : γFilter α} {g : γSet αFilter β} (hf : Monotone f) (hg : Monotone g) :
Monotone fun c => Filter.lift (f c) (g c)
theorem Filter.lift_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set αFilter β} (hm : Monotone g) :
Filter.NeBot (Filter.lift f g) ∀ (s : Set α), s fFilter.NeBot (g s)
@[simp]
theorem Filter.lift_const {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
(Filter.lift f fun x => g) = g
@[simp]
theorem Filter.lift_inf {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set αFilter β} {h : Set αFilter β} :
(Filter.lift f fun x => g x h x) = Filter.lift f g Filter.lift f h
@[simp]
theorem Filter.lift_principal2 {α : Type u_1} {f : Filter α} :
Filter.lift f Filter.principal = f
theorem Filter.lift_infᵢ_le {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : ιFilter α} {g : Set αFilter β} :
Filter.lift (infᵢ f) g i, Filter.lift (f i) g
theorem Filter.lift_infᵢ {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : Nonempty ι] {f : ιFilter α} {g : Set αFilter β} (hg : ∀ (s t : Set α), g (s t) = g s g t) :
Filter.lift (infᵢ f) g = i, Filter.lift (f i) g
theorem Filter.lift_infᵢ_of_directed {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : Nonempty ι] {f : ιFilter α} {g : Set αFilter β} (hf : Directed (fun x x_1 => x x_1) f) (hg : Monotone g) :
Filter.lift (infᵢ f) g = i, Filter.lift (f i) g
theorem Filter.lift_infᵢ_of_map_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : ιFilter α} {g : Set αFilter β} (hg : ∀ (s t : Set α), g (s t) = g s g t) (hg' : g Set.univ = ) :
Filter.lift (infᵢ f) g = i, Filter.lift (f i) g
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) :
theorem Filter.tendsto_lift' {α : Type u_3} {β : Type u_2} {γ : Type u_1} {f : Filter α} {h : Set αSet β} {m : γβ} {l : Filter γ} :
Filter.Tendsto m l (Filter.lift' f h) ∀ (s : Set α), s fFilter.Eventually (fun a => m a h s) l
theorem Filter.HasBasis.lift' {α : Type u_2} {β : Type u_3} {f : Filter α} {h : Set αSet β} {ι : Sort u_1} {p : ιProp} {s : ιSet α} (hf : Filter.HasBasis f p s) (hh : Monotone h) :
theorem Filter.mem_lift'_sets {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set αSet β} (hh : Monotone h) {s : Set β} :
s Filter.lift' f h t, 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} :
Filter.Eventually (fun y => p y) (Filter.lift' f h) t, t f ((y : β) → y h tp y)
theorem Filter.interₛ_lift'_sets {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set αSet β} (hh : Monotone h) :
⋂₀ { s | s Filter.lift' f h } = Set.interᵢ fun s => Set.interᵢ fun h => 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) :
theorem Filter.lift'_mono {α : Type u_1} {β : Type u_2} {f₁ : Filter α} {f₂ : Filter α} {h₁ : Set αSet β} {h₂ : Set αSet β} (hf : f₁ f₂) (hh : h₁ h₂) :
Filter.lift' f₁ h₁ Filter.lift' f₂ h₂
theorem Filter.lift'_mono' {α : Type u_1} {β : Type u_2} {f : Filter α} {h₁ : Set αSet β} {h₂ : Set αSet β} (hh : ∀ (s : Set α), s fh₁ s h₂ s) :
theorem Filter.lift'_cong {α : Type u_1} {β : Type u_2} {f : Filter α} {h₁ : Set αSet β} {h₂ : Set αSet β} (hh : ∀ (s : Set α), s fh₁ s = h₂ s) :
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_3} {β : Type u_1} {γ : Type u_2} {f : Filter α} {g : Set βSet γ} {m : αβ} :
theorem Filter.map_lift'_eq2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : Filter α} {g : Set βSet γ} {m : αβ} (hg : Monotone g) :
theorem Filter.comap_lift'_eq {α : Type u_3} {β : Type u_2} {γ : Type u_1} {f : Filter α} {h : Set αSet β} {m : γβ} :
theorem Filter.comap_lift'_eq2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} {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 Filter.lift' f h ∀ (s : Set α), s fh s g
theorem Filter.principal_le_lift' {α : Type u_2} {β : Type u_1} {f : Filter α} {h : Set αSet β} {t : Set β} :
Filter.principal t Filter.lift' f h ∀ (s : Set α), s ft h s
theorem Filter.monotone_lift' {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : Preorder γ] {f : γFilter α} {g : γSet αSet β} (hf : Monotone f) (hg : Monotone g) :
Monotone fun c => Filter.lift' (f c) (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) :
Filter.lift (Filter.lift' f g) h = Filter.lift f fun s => 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) :
Filter.lift' (Filter.lift' f g) h = Filter.lift' f fun s => 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) :
theorem Filter.lift_lift'_same_le_lift' {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set αSet αSet β} :
(Filter.lift f fun s => Filter.lift' f (g s)) Filter.lift' f fun s => 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 fun t => g s t) (hg₂ : ∀ (t : Set α), Monotone fun s => g s t) :
(Filter.lift f fun s => Filter.lift' f (g s)) = Filter.lift' f fun s => g s s
theorem Filter.lift'_inf_principal_eq {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set αSet β} {s : Set β} :
theorem Filter.lift'_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set αSet β} (hh : Monotone h) :
Filter.NeBot (Filter.lift' f h) ∀ (s : Set α), s fSet.Nonempty (h s)
@[simp]
theorem Filter.lift'_id {α : Type u_1} {f : Filter α} :
theorem Filter.lift'_infᵢ {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : Nonempty ι] {f : ιFilter α} {g : Set αSet β} (hg : ∀ (s t : Set α), g (s t) = g s g t) :
Filter.lift' (infᵢ f) g = i, Filter.lift' (f i) g
theorem Filter.lift'_infᵢ_of_map_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : ιFilter α} {g : Set αSet β} (hg : ∀ {s t : Set α}, g (s t) = g s g t) (hg' : g Set.univ = Set.univ) :
Filter.lift' (infᵢ f) g = i, Filter.lift' (f i) g
theorem Filter.lift'_inf {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter α) {s : Set αSet β} (hs : ∀ (t₁ t₂ : Set α), s (t₁ t₂) = s t₁ s t₂) :
theorem Filter.lift'_inf_le {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter α) (s : Set αSet β) :
theorem Filter.comap_eq_lift' {α : Type u_2} {β : Type u_1} {f : Filter β} {m : αβ} :
theorem Filter.prod_def {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} :
Filter.prod f g = Filter.lift f fun s => Filter.lift' g fun t => s ×ˢ t
theorem Filter.mem_prod_same_iff {α : Type u_1} {la : Filter α} {s : Set (α × α)} :
s Filter.prod la la t, t la t ×ˢ t s

Alias of Filter.mem_prod_self_iff.

theorem Filter.prod_same_eq {α : Type u_1} {f : Filter α} :
Filter.prod f f = Filter.lift' f fun t => t ×ˢ t
theorem Filter.tendsto_prod_self_iff {α : Type u_1} {β : Type u_2} {f : α × αβ} {x : Filter α} {y : Filter β} :
Filter.Tendsto f (Filter.prod x x) y ∀ (W : Set β), W yU, U x ∀ (x x' : α), x Ux' Uf (x, x') W
theorem Filter.prod_lift_lift {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {f₁ : Filter α₁} {f₂ : Filter α₂} {g₁ : Set α₁Filter β₁} {g₂ : Set α₂Filter β₂} (hg₁ : Monotone g₁) (hg₂ : Monotone g₂) :
Filter.prod (Filter.lift f₁ g₁) (Filter.lift f₂ g₂) = Filter.lift f₁ fun s => Filter.lift f₂ fun t => Filter.prod (g₁ s) (g₂ t)
theorem Filter.prod_lift'_lift' {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {f₁ : Filter α₁} {f₂ : Filter α₂} {g₁ : Set α₁Set β₁} {g₂ : Set α₂Set β₂} (hg₁ : Monotone g₁) (hg₂ : Monotone g₂) :
Filter.prod (Filter.lift' f₁ g₁) (Filter.lift' f₂ g₂) = Filter.lift f₁ fun s => Filter.lift' f₂ fun t => g₁ s ×ˢ g₂ t