case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.124763
ι✝ : Sort x
f✝ g : Filter α
s✝ t : Set α
ι : Type w
f : ι → Set α
s : Finset ι
⊢ (⨅ (i : ι) (_ : i ∈ ↑s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ ↑s), f i)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.124763
ι✝ : Sort x
f✝ g : Filter α
s✝ t : Set α
ι : Type w
s : Set ι
hs : Set.Finite s
f : ι → Set α
⊢ (⨅ (i : ι) (_ : i ∈ s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ s), f i)
lift s to Finset ι using hs
no goals
case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.124763
ι✝ : Sort x
f✝ g : Filter α
s✝ t : Set α
ι : Type w
f : ι → Set α
s : Finset ι
⊢ (⨅ (i : ι) (_ : i ∈ ↑s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ ↑s), f i)
exact_mod_cast iInf_principal_finset s f