case inl
α : Type u_1
β : Type u_2
γ : Type ?u.26409
ι : Sort u_3
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : IsEmpty ι
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.26409
ι : Sort u_3
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
α : Type u_1
β : Type u_2
γ : Type ?u.26409
ι : Sort u_3
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
cases isEmpty_or_nonempty ι
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.26409
ι : Sort u_3
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : IsEmpty ι
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
simp [iInf_of_empty, hg']
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.26409
ι : Sort u_3
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
exact lift_iInf hg