α : Type u
β : Type v
γ : Type w
δ : Type ?u.101802
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
⊢ (⨅ (x : PLift ι), f (↑Equiv.plift x)).sets = (⨅ (i : PLift ι), f i.down).sets
α : Type u
β : Type v
γ : Type w
δ : Type ?u.101802
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
⊢ (⨅ (i : ι), f i).sets = ⋃ (t : Finset (PLift ι)), (⨅ (i : PLift ι) (_ : i ∈ t), f i.down).sets
rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.101802
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
⊢ (⨅ (x : PLift ι), f (↑Equiv.plift x)).sets = (⨅ (i : PLift ι), f i.down).sets
rfl