case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.122731
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
⊢ (⨅ (i : ι), 𝓟 (f i)) = 𝓟 (⋂ (i : ι), f i)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.122731
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type w
inst✝ : Finite ι
f : ι → Set α
⊢ (⨅ (i : ι), 𝓟 (f i)) = 𝓟 (⋂ (i : ι), f i)
cases nonempty_fintype ι
no goals
case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.122731
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
⊢ (⨅ (i : ι), 𝓟 (f i)) = 𝓟 (⋂ (i : ι), f i)
simpa using iInf_principal_finset Finset.univ f