Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2019 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
! This file was ported from Lean 3 source module order.filter.lift
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Filter.Bases
import Mathlib.Order.ConditionallyCompleteLattice.Basic
/-!
# Lift filters along filter and set functions
-/
open Set Classical Filter Function
namespace Filter
variable { α β γ : Type _ : Type (?u.43803+1)} { ι : Sort _ }
section lift
/-- 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. -/
protected def lift ( f : Filter α ) ( g : Set α → Filter β ) :=
⨅ s ∈ f , g s
#align filter.lift Filter.lift
variable { f f₁ f₂ : Filter α } { g g₁ g₂ : Set α → Filter β }
@[ simp ]
theorem lift_top ( g : Set α → Filter β ) : ( ⊤ : Filter α ). lift g = g univ := by simp [ Filter.lift ]
#align filter.lift_top Filter.lift_top
-- porting note: use `∃ i, p i ∧ _` instead of `∃ i (hi : p i), _`
/-- 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 HasBasis.mem_lift_iff { ι } { p : ι → Prop } { s : ι → Set α } { f : Filter α }
( hf : f . HasBasis p s ) { β : ι → Type _ } { pg : ∀ i , β i → Prop } { sg : (i : ι ) → β i Set γ sg : ∀ i , β i → Set γ }
{ g : Set α → Filter γ } ( hg : ∀ (i : ι ), HasBasis (g (s i pg i sg i hg : ∀ i , ( g <| s i ). HasBasis ( pg i ) ( sg : (i : ι ) → β i Set γ sg i )) ( gm : Monotone g )
{ s : Set γ } : s ∈ f . lift g ↔ ∃ i , p i ∧ ∃ x , pg i x ∧ sg : (i : ι ) → β i Set γ sg i x ⊆ s := by
refine' ( mem_biInf_of_directed _ ⟨ univ , univ_sets : ∀ {α : Type ?u.3153} (self : Filter α univ ∈ self .sets _ ⟩). trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c trans _ refine'_1 refine'_2 (∃ i , i ∈ f .sets∧ s ∈ g i ) ↔ ∃ i , p i ∧ ∃ x , pg i x ∧ sg i x ⊆ s
· refine'_1 refine'_2 (∃ i , i ∈ f .sets∧ s ∈ g i ) ↔ ∃ i , p i ∧ ∃ x , pg i x ∧ sg i x ⊆ s intro t₁ ht₁ t₂ ht₂
exact ⟨ t₁ ∩ t₂ , inter_mem : ∀ {α : Type ?u.3293} {f : Filter α s t : Set α s ∈ f t ∈ f s ∩ t ∈ f ht₁ ht₂ , gm <| inter_subset_left : ∀ {α : Type ?u.3320} (s t : Set α s ∩ t ⊆ s _ _ , gm <| inter_subset_right : ∀ {α : Type ?u.3343} (s t : Set α s ∩ t ⊆ t _ _ ⟩
· refine'_2 (∃ i , i ∈ f .sets∧ s ∈ g i ) ↔ ∃ i , p i ∧ ∃ x , pg i x ∧ sg i x ⊆ s refine'_2 (∃ i , i ∈ f .sets∧ s ∈ g i ) ↔ ∃ i , p i ∧ ∃ x , pg i x ∧ sg i x ⊆ s simp only [← ( hg : ∀ (i : ι ), HasBasis (g (s✝ i pg i sg i hg _ ). mem_iff ] refine'_2 (∃ i , i ∈ f .sets∧ s ∈ g i ) ↔ ∃ i , p i ∧ s ∈ g (s✝ i
refine'_2 (∃ i , i ∈ f .sets∧ s ∈ g i ) ↔ ∃ i , p i ∧ ∃ x , pg i x ∧ sg i x ⊆ s exact hf . exists_iff fun t₁ t₂ ht H => gm ht H
#align filter.has_basis.mem_lift_iff Filter.HasBasis.mem_lift_iffₓ
/-- 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 HasBasis.lift { ι } { p : ι → Prop } { s : ι → Set α } { f : Filter α } ( hf : f . HasBasis p s )
{ β : ι → Type _ } { pg : ∀ i , β i → Prop } { sg : (i : ι ) → β i Set γ sg : ∀ i , β i → Set γ } { g : Set α → Filter γ }
( hg : ∀ (i : ι ), HasBasis (g (s i pg i sg i hg : ∀ i , ( g ( s i )). HasBasis ( pg i ) ( sg : (i : ι ) → β i Set γ sg i )) ( gm : Monotone g ) :
( f . lift g ). HasBasis ( fun i : Σ i , β i => p i . 1 ∧ pg i . 1 i . 2 : {α : Type ?u.4058} → {β : α → Type ?u.4057(self : Sigma β β self .fst ) fun i : Σ i , β i => sg : (i : ι ) → β i Set γ sg i . 1 i . 2 : {α : Type ?u.4084} → {β : α → Type ?u.4083(self : Sigma β β self .fst := by
refine' ⟨ fun t => ( hf . mem_lift_iff hg : ∀ (i : ι ), HasBasis (g (s i pg i sg i hg gm ). trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c trans _ ⟩ (∃ i , p i ∧ ∃ x , pg i x ∧ sg i x ⊆ t ) ↔ ∃ i , (p i .fst∧ pg i .fsti .snd∧ sg i .fsti .snd⊆ t
simp [ Sigma.exists : ∀ {α : Type ?u.4250} {β : α → Type ?u.4251p : (a : α ) × β a → Prop (∃ x , p x ) ↔ ∃ a b , p { fst := a , snd := b } , and_assoc : ∀ {a b c : Prop }, (a ∧ b ∧ c ↔ a ∧ b ∧ c , exists_and_left : ∀ {α : Sort ?u.4288} {p : α → Prop b : Prop }, (∃ x , b ∧ p x ) ↔ b ∧ ∃ x , p x ]
#align filter.has_basis.lift Filter.HasBasis.lift
theorem mem_lift_sets ( hg : Monotone g ) { s : Set β } : s ∈ f . lift g ↔ ∃ t ∈ f , s ∈ g t :=
( f . basis_sets . mem_lift_iff ( fun s => ( g s ). basis_sets ) hg ). trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c trans <| by
(∃ i , i ∈ f ∧ ∃ x , x ∈ g i ∧ id x ⊆ s ) ↔ ∃ t , t ∈ f ∧ s ∈ g t simp only [ id : {α : Sort ?u.8551} → α → α , exists_mem_subset_iff : ∀ {α : Type ?u.8555} {f : Filter α s : Set α (∃ t , t ∈ f ∧ t ⊆ s ) ↔ s ∈ f ]
#align filter.mem_lift_sets Filter.mem_lift_sets
theorem sInter_lift_sets ( hg : Monotone g ) :
⋂₀ { s | s ∈ f . lift g } = ⋂ s ∈ f , ⋂₀ { t | t ∈ g s } := by
simp only [ sInter_eq_biInter , mem_setOf_eq : ∀ {α : Type ?u.9138} {x : α } {p : α → Prop (x ∈ { y | p y = p x , Filter.mem_sets : ∀ {α : Type ?u.9155} {f : Filter α s : Set α s ∈ f .sets↔ s ∈ f , mem_lift_sets hg , iInter_exists ,
iInter_and , @ iInter_comm _ ( Set β )]
#align filter.sInter_lift_sets Filter.sInter_lift_sets
theorem mem_lift { s : Set β } { t : Set α } ( ht : t ∈ f ) ( hs : s ∈ g t ) : s ∈ f . lift g :=
le_principal_iff . mp : ∀ {a b : Prop }, (a ↔ b a → b <|
show f . lift g ≤ 𝓟 s from iInf_le_of_le t <| iInf_le_of_le ht <| le_principal_iff . mpr : ∀ {a b : Prop }, (a ↔ b b → a hs
#align filter.mem_lift Filter.mem_lift
theorem lift_le { f : Filter α } { g : Set α → Filter β } { h : Filter β } { s : Set α } ( hs : s ∈ f )
( hg : g s ≤ h ) : f . lift g ≤ h :=
iInf₂_le_of_le : ∀ {α : Type ?u.11478} {ι : Sort ?u.11479} {κ : ι → Sort ?u.11480inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α } (i : ι ) (j : κ i f i j ≤ a (⨅ i , ⨅ j , f i j ) ≤ a s hs hg
#align filter.lift_le Filter.lift_le
theorem le_lift { f : Filter α } { g : Set α → Filter β } { h : Filter β } :
h ≤ f . lift g ↔ ∀ s ∈ f , h ≤ g s :=
le_iInf₂_iff : ∀ {α : Type ?u.11748} {ι : Sort ?u.11749} {κ : ι → Sort ?u.11750inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α }, (a ≤ ⨅ i , ⨅ j , f i j ↔ ∀ (i : ι ) (j : κ i a ≤ f i j
#align filter.le_lift Filter.le_lift
theorem lift_mono ( hf : f₁ ≤ f₂ ) ( hg : g₁ ≤ g₂ ) : f₁ . lift g₁ ≤ f₂ . lift g₂ :=
iInf_mono fun s => iInf_mono' fun hs => ⟨ hf hs , hg s ⟩
#align filter.lift_mono Filter.lift_mono
theorem lift_mono' ( hg : ∀ (s : Set α s ∈ f g₁ s ≤ g₂ s hg : ∀ s ∈ f , g₁ s ≤ g₂ s ) : f . lift g₁ ≤ f . lift g₂ := iInf₂_mono : ∀ {α : Type ?u.12379} {ι : Sort ?u.12380} {κ : ι → Sort ?u.12381inst : CompleteLattice α f g : (i : ι ) → κ i α },
(∀ (i : ι ) (j : κ i f i j ≤ g i j ) → (⨅ i , ⨅ j , f i j ) ≤ ⨅ i , ⨅ j , g i j hg : ∀ (s : Set α s ∈ f g₁ s ≤ g₂ s hg
#align filter.lift_mono' Filter.lift_mono'
theorem tendsto_lift { m : γ → β } { l : Filter γ } :
Tendsto m l ( f . lift g ) ↔ ∀ s ∈ f , Tendsto m l ( g s ) := by
simp only [ Filter.lift , tendsto_iInf ]
#align filter.tendsto_lift Filter.tendsto_lift
theorem map_lift_eq { m : β → γ } ( hg : Monotone g ) : map m ( f . lift g ) = f . lift ( map m ∘ g ) :=
have : Monotone ( map m ∘ g ) := map_mono . comp hg
Filter.ext : ∀ {α : Type ?u.13528} {f g : Filter α (∀ (s : Set α s ∈ f ↔ s ∈ g ) → f = g fun s => by
simp only [ mem_lift_sets hg , mem_lift_sets this , exists_prop : ∀ {b a : Prop }, (∃ _h , b ) ↔ a ∧ b , mem_map , Function.comp_apply : ∀ {β : Sort ?u.13712} {δ : Sort ?u.13713} {α : Sort ?u.13714} {f : β → δ g : α → β x : α }, (f ∘ g ) x = f (g x ]
#align filter.map_lift_eq Filter.map_lift_eq
theorem comap_lift_eq { m : γ → β } : comap m ( f . lift g ) = f . lift ( comap m ∘ g ) := by
simp only [ Filter.lift , comap_iInf : ∀ {α : Type ?u.14216} {β : Type ?u.14215} {ι : Sort ?u.14214} {m : α → β f : ι → Filter β comap m (⨅ i , f i )= ⨅ i , comap m (f i ] ; rfl
#align filter.comap_lift_eq Filter.comap_lift_eq
theorem comap_lift_eq2 { m : β → α } { g : Set β → Filter γ } ( hg : Monotone g ) :
( comap m f ). lift g = f . lift ( g ∘ preimage : {α : Type ?u.15042} → {β : Type ?u.15041} → (α → β Set β Set α m ) :=
le_antisymm ( le_iInf₂ : ∀ {α : Type ?u.15116} {ι : Sort ?u.15117} {κ : ι → Sort ?u.15118inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α }, (∀ (i : ι ) (j : κ i a ≤ f i j ) → a ≤ ⨅ i , ⨅ j , f i j fun s hs => iInf₂_le : ∀ {α : Type ?u.15210} {ι : Sort ?u.15211} {κ : ι → Sort ?u.15212inst : CompleteLattice α f : (i : ι ) → κ i α }
(i : ι ) (j : κ i (⨅ i , ⨅ j , f i j ) ≤ f i j ( m ⁻¹' s ) ⟨ s , hs , Subset.rfl : ∀ {α : Type ?u.15488} {s : Set α s ⊆ s ⟩)
( le_iInf₂ : ∀ {α : Type ?u.15326} {ι : Sort ?u.15327} {κ : ι → Sort ?u.15328inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α }, (∀ (i : ι ) (j : κ i a ≤ f i j ) → a ≤ ⨅ i , ⨅ j , f i j fun _s ⟨ s' , hs' , h_sub ⟩ => iInf₂_le_of_le : ∀ {α : Type ?u.15411} {ι : Sort ?u.15412} {κ : ι → Sort ?u.15413inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α } (i : ι ) (j : κ i f i j ≤ a (⨅ i , ⨅ j , f i j ) ≤ a s' hs' <| hg h_sub )
#align filter.comap_lift_eq2 Filter.comap_lift_eq2
theorem lift_map_le { g : Set β → Filter γ } { m : α → β } : ( map m f ). lift g ≤ f . lift ( g ∘ image : {α : Type ?u.15792} → {β : Type ?u.15791} → (α → β Set α Set β m ) :=
le_lift . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _s hs => lift_le ( image_mem_map : ∀ {α : Type ?u.15909} {β : Type ?u.15908} {f : Filter α m : α → β s : Set α s ∈ f m '' s ∈ map m f hs ) le_rfl
#align filter.lift_map_le Filter.lift_map_le
theorem map_lift_eq2 { g : Set β → Filter γ } { m : α → β } ( hg : Monotone g ) :
( map m f ). lift g = f . lift ( g ∘ image : {α : Type ?u.16239} → {β : Type ?u.16238} → (α → β Set α Set β m ) :=
lift_map_le . antisymm <| le_lift . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _s hs => lift_le hs <| hg <| image_preimage_subset : ∀ {α : Type ?u.16412} {β : Type ?u.16411} (f : α → β s : Set β f '' (f ⁻¹' s ⊆ s _ _
#align filter.map_lift_eq2 Filter.map_lift_eq2
theorem lift_comm { g : Filter β } { h : Set α → Set β → Filter γ } :
( f . lift fun s => g . lift ( h s )) = g . lift fun t => f . lift fun s => h s t :=
le_antisymm
( le_iInf fun i => le_iInf fun hi => le_iInf fun j => le_iInf fun hj =>
iInf_le_of_le j <| iInf_le_of_le hj <| iInf_le_of_le i <| iInf_le _ hi )
( le_iInf fun i => le_iInf fun hi => le_iInf fun j => le_iInf fun hj =>
iInf_le_of_le j <| iInf_le_of_le hj <| iInf_le_of_le i <| iInf_le _ hi )
#align filter.lift_comm Filter.lift_comm
theorem lift_assoc { h : Set β → Filter γ } ( hg : Monotone g ) :
( f . lift g ). lift h = f . lift fun s => ( g s ). lift h :=
le_antisymm
( le_iInf₂ : ∀ {α : Type ?u.17652} {ι : Sort ?u.17653} {κ : ι → Sort ?u.17654inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α }, (∀ (i : ι ) (j : κ i a ≤ f i j ) → a ≤ ⨅ i , ⨅ j , f i j fun _s hs => le_iInf₂ : ∀ {α : Type ?u.17747} {ι : Sort ?u.17748} {κ : ι → Sort ?u.17749inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α }, (∀ (i : ι ) (j : κ i a ≤ f i j ) → a ≤ ⨅ i , ⨅ j , f i j fun t ht =>
iInf_le_of_le t <| iInf_le _ <| ( mem_lift_sets hg ). mpr : ∀ {a b : Prop }, (a ↔ b b → a mpr ⟨ _ , hs , ht ⟩)
( le_iInf₂ : ∀ {α : Type ?u.18001} {ι : Sort ?u.18002} {κ : ι → Sort ?u.18003inst : CompleteLattice α a : α }
{f : (i : ι ) → κ i α }, (∀ (i : ι ) (j : κ i a ≤ f i j ) → a ≤ ⨅ i , ⨅ j , f i j fun t ht =>
let ⟨ s , hs , h' ⟩ := ( mem_lift_sets hg ). mp : ∀ {a b : Prop }, (a ↔ b a → b mp ht
iInf_le_of_le s <| iInf_le_of_le hs <| iInf_le_of_le t <| iInf_le _ h' )
#align filter.lift_assoc Filter.lift_assoc
theorem lift_lift_same_le_lift { g : Set α → Set α → Filter β } :
( f . lift fun s => f . lift ( g s )) ≤ f . lift fun s => g s s :=
le_lift . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _s hs => lift_le hs <| lift_le hs le_rfl
#align filter.lift_lift_same_le_lift Filter.lift_lift_same_le_lift
theorem lift_lift_same_eq_lift { g : Set α → Set α → Filter β } ( hg₁ : ∀ s , Monotone fun t => g s t )
( hg₂ : ∀ t , Monotone fun s => g s t ) : ( f . lift fun s => f . lift ( g s )) = f . lift fun s => g s s :=
lift_lift_same_le_lift . antisymm <|
le_lift . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun s hs => le_lift . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun t ht => lift_le ( inter_mem : ∀ {α : Type ?u.19204} {f : Filter α s t : Set α s ∈ f t ∈ f s ∩ t ∈ f hs ht ) <|
calc
g ( s ∩ t ) ( s ∩ t ) ≤ g s ( s ∩ t ) := hg₂ ( s ∩ t ) ( inter_subset_left : ∀ {α : Type ?u.19317} (s t : Set α s ∩ t ⊆ s _ _ )
_ ≤ g s t := hg₁ s ( inter_subset_right : ∀ {α : Type ?u.19360} (s t : Set α s ∩ t ⊆ t _ _ )
#align filter.lift_lift_same_eq_lift Filter.lift_lift_same_eq_lift
theorem lift_principal { s : Set α } ( hg : Monotone g ) : ( 𝓟 s ). lift g = g s :=
( lift_le ( mem_principal_self : ∀ {α : Type ?u.19698} (s : Set α s ∈ 𝓟 s _ ) le_rfl ). antisymm ( le_lift . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _t ht => hg ht )
#align filter.lift_principal Filter.lift_principal
theorem monotone_lift [ Preorder γ ] { f : γ → Filter α } { g : γ → Set α → Filter β } ( hf : Monotone f )
( hg : Monotone g ) : Monotone fun c => ( f c ). lift ( g c ) := fun _ _ h => lift_mono ( hf h ) ( hg h )
#align filter.monotone_lift Filter.monotone_lift
theorem lift_neBot_iff ( hm : Monotone g ) : ( NeBot ( f . lift g )) ↔ ∀ s ∈ f , NeBot ( g s ) := by
simp only [ neBot_iff , Ne.def : ∀ {α : Sort ?u.20597} (a b : α ), (a ≠ b = ¬ a = b , ← empty_mem_iff_bot , mem_lift_sets hm , not_exists : ∀ {α : Sort ?u.20684} {p : α → Prop (¬ ∃ x , p x ↔ ∀ (x : α ), ¬ p x , not_and : ∀ {a b : Prop }, ¬ (a ∧ b ↔ a → ¬ b ]
#align filter.lift_ne_bot_iff Filter.lift_neBot_iff
@[ simp ]
theorem lift_const { f : Filter α } { g : Filter β } : ( f . lift fun _ => g ) = g :=
iInf_subtype' : ∀ {α : Type ?u.21074} {ι : Sort ?u.21075} [inst : CompleteLattice α p : ι → Prop f : (i : ι ) → p i α },
(⨅ i , ⨅ h , f i h ) = ⨅ x , f ↑x (_ : p ↑x . trans : ∀ {α : Sort ?u.21097} {a b c : α }, a = b b = c a = c iInf_const
#align filter.lift_const Filter.lift_const
@[ simp ]
theorem lift_inf { f : Filter α } { g h : Set α → Filter β } :
( f . lift fun x => g x ⊓ h x ) = f . lift g ⊓ f . lift h := by simp only [ Filter.lift , iInf_inf_eq : ∀ {α : Type ?u.21596} {ι : Sort ?u.21597} [inst : CompleteLattice α f g : ι → α (⨅ x , f x ⊓ g x ) = (⨅ x , f x ) ⊓ ⨅ x , g x ]
#align filter.lift_inf Filter.lift_inf
@[ simp ]
theorem lift_principal2 { f : Filter α } : f . lift 𝓟 = f :=
le_antisymm ( fun s hs => mem_lift hs ( mem_principal_self : ∀ {α : Type ?u.22590} (s : Set α s ∈ 𝓟 s s ))
( le_iInf fun s => le_iInf fun hs => by simp only [ hs , le_principal_iff ] )
#align filter.lift_principal2 Filter.lift_principal2
theorem lift_iInf_le { f : ι → Filter α } { g : Set α → Filter β } :
( iInf : {α : Type ?u.22965} → [inst : InfSet α {ι : Sort ?u.22964} → (ι → α α f ). lift g ≤ ⨅ i , ( f i ). lift g :=
le_iInf fun _ => lift_mono ( iInf_le _ _ ) le_rfl
#align filter.lift_infi_le Filter.lift_iInf_le
theorem lift_iInf [ Nonempty ι ] { f : ι → Filter α } { g : Set α → Filter β }
( hg : ∀ (s t : Set α g (s ∩ t = g s ⊓ g t hg : ∀ s t , g ( s ∩ t ) = g s ⊓ g t ) : ( iInf : {α : Type ?u.23469} → [inst : InfSet α {ι : Sort ?u.23468} → (ι → α α f ). lift g = ⨅ i , ( f i ). lift g := by
refine' lift_iInf_le . antisymm fun s => _ : s ∈ ?m.23607 s ∈ ?m.23608
have H : ∀ t ∈ iInf : {α : Type ?u.23696} → [inst : InfSet α {ι : Sort ?u.23695} → (ι → α α f , (⨅ i , ( f i ). lift g ) ≤ g t := by
intro t ht
refine' iInf_sets_induct : ∀ {α : Type ?u.23870} {ι : Sort ?u.23869} {f : ι → Filter α s : Set α s ∈ iInf f ∀ {p : Set α Prop p univ (∀ {i : ι } {s₁ s₂ : Set α s₁ ∈ f i p s₂ p (s₁ ∩ s₂ ) → p s ht _ fun hs ht => _
· inhabit ι