Lift filters along filter and set functions

def Filter.lift {α : Type u_1} {β : Type u_2} (f : Filter α) (g : 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

• Filter.lift f g = ⨅ (s : Set α) (_ : s ∈ f), g s

@[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_1} {γ : Type u_3} {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α} (hf : Filter.HasBasis f p s) {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {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_1} {γ : Type u_3} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α} (hf : Filter.HasBasis f p s) {β : ι → Type u_5} {pg : (i : ι) → β i → Prop} {sg : (i : ι) → β i → Set γ} {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.sInter_lift_sets {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β} (hg : Monotone g) : ⋂₀ {s | s ∈ Filter.lift f g} = ⋂ (s : Set α) (_ : s ∈ f), ⋂₀ {t | 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 ∈ Filter.lift f 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) : Filter.lift f g ≤ 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 ∈ f → h ≤ 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 ∈ f → g₁ s ≤ g₂ s) : Filter.lift f g₁ ≤ Filter.lift f 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 (Filter.lift f 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) : Filter.map m (Filter.lift f g) = Filter.lift f (Filter.map m ∘ g)

theorem Filter.comap_lift_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {m : γ → β} : Filter.comap m (Filter.lift f g) = Filter.lift f (Filter.comap m ∘ g)

theorem Filter.comap_lift_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Filter γ} (hg : Monotone g) : Filter.lift (Filter.comap m f) g = Filter.lift f (g ∘ Set.preimage m)

theorem Filter.lift_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Filter γ} {m : α → β} : Filter.lift (Filter.map m f) g ≤ Filter.lift f (g ∘ Set.image 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.lift (Filter.map m f) g = Filter.lift f (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 γ} : (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_1} {β : Type u_2} {γ : Type u_3} {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) : Filter.lift (Filter.principal s) g = g s

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 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 ∈ f → Filter.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_iInf_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → Filter α} {g : Set α → Filter β} : Filter.lift (iInf f) g ≤ ⨅ (i : ι), Filter.lift (f i) g

theorem Filter.lift_iInf {α : 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) : Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g

theorem Filter.lift_iInf_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β} (hf : Directed (fun x x_1 => x ≥ x_1) f) (hg : Monotone g) : Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g

theorem Filter.lift_iInf_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 = ⊤) : Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g

def Filter.lift' {α : Type u_1} {β : Type u_2} (f : Filter α) (h : 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

• Filter.lift' f h = Filter.lift f (Filter.principal ∘ h)

@[simp]

theorem Filter.lift'_top {α : Type u_1} {β : Type u_2} (h : Set α → Set β) : Filter.lift' ⊤ h = Filter.principal (h Set.univ)

theorem Filter.mem_lift' {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {t : Set α} (ht : t ∈ f) : h t ∈ Filter.lift' f 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 (Filter.lift' f h) ↔ ∀ (s : Set α), s ∈ f → ∀ᶠ (a : γ) in l, m a ∈ h s

theorem Filter.HasBasis.lift' {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} (hf : Filter.HasBasis f p s) (hh : Monotone h) : Filter.HasBasis (Filter.lift' f h) 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 ∈ 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} : (∀ᶠ (y : β) in Filter.lift' f h, p y) ↔ ∃ t, 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 | s ∈ Filter.lift' f h} = ⋂ (s : Set α) (_ : 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) : Filter.lift' f g ≤ 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 ∈ f → h₁ s ⊆ h₂ s) : Filter.lift' f h₁ ≤ Filter.lift' f h₂

theorem Filter.lift'_cong {α : Type u_1} {β : Type u_2} {f : Filter α} {h₁ : Set α → Set β} {h₂ : Set α → Set β} (hh : ∀ (s : Set α), s ∈ f → h₁ s = h₂ s) : Filter.lift' f h₁ = Filter.lift' f h₂

theorem Filter.map_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : β → γ} (hh : Monotone h) : Filter.map m (Filter.lift' f h) = Filter.lift' f (Set.image m ∘ h)

theorem Filter.lift'_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β} : Filter.lift' (Filter.map m f) g ≤ Filter.lift' f (g ∘ Set.image m)

theorem Filter.map_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β} (hg : Monotone g) : Filter.lift' (Filter.map m f) g = Filter.lift' f (g ∘ Set.image m)

theorem Filter.comap_lift'_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : γ → β} : Filter.comap m (Filter.lift' f h) = Filter.lift' f (Set.preimage m ∘ h)

theorem Filter.comap_lift'_eq2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Set γ} (hg : Monotone g) : Filter.lift' (Filter.comap m f) g = Filter.lift' f (g ∘ Set.preimage m)

theorem Filter.lift'_principal {α : Type u_1} {β : Type u_2} {h : Set α → Set β} {s : Set α} (hh : Monotone h) : Filter.lift' (Filter.principal s) h = Filter.principal (h s)

theorem Filter.lift'_pure {α : Type u_1} {β : Type u_2} {h : Set α → Set β} {a : α} (hh : Monotone h) : Filter.lift' (pure a) h = Filter.principal (h {a})

theorem Filter.lift'_bot {α : Type u_1} {β : Type u_2} {h : Set α → Set β} (hh : Monotone h) : Filter.lift' ⊥ h = Filter.principal (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 ∈ 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 ≤ Filter.lift' f 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 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) : 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 α → 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 β} : Filter.lift' f h ⊓ Filter.principal s = Filter.lift' f fun t => h t ∩ s

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 ∈ f → Set.Nonempty (h s)

@[simp]

theorem Filter.lift'_id {α : Type u_1} {f : Filter α} : Filter.lift' f id = f

theorem Filter.lift'_iInf {α : 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) : Filter.lift' (iInf f) g = ⨅ (i : ι), Filter.lift' (f i) g

theorem Filter.lift'_iInf_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) : Filter.lift' (iInf 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₂) : Filter.lift' (f ⊓ g) s = Filter.lift' f s ⊓ Filter.lift' g s

theorem Filter.lift'_inf_le {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter α) (s : Set α → Set β) : Filter.lift' (f ⊓ g) s ≤ Filter.lift' f s ⊓ Filter.lift' g s

theorem Filter.comap_eq_lift' {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : Filter.comap m f = Filter.lift' f (Set.preimage m)

theorem Filter.prod_def {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : 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 ∈ 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 α} : 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 (x ×ˢ x) y ↔ ∀ (W : Set β), W ∈ y → ∃ U, 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₂) : Filter.lift f₁ g₁ ×ˢ Filter.lift f₂ g₂ = Filter.lift f₁ fun s => Filter.lift f₂ fun t => 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₂) : Filter.lift' f₁ g₁ ×ˢ Filter.lift' f₂ g₂ = Filter.lift f₁ fun s => Filter.lift' f₂ fun t => g₁ s ×ˢ g₂ t