ι✝ : Sort ?u.642
α : Type u_2
β : Type ?u.648
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
ι✝ : Sort ?u.642
α : Type u_2
β : Type ?u.648
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
⊢ (⋂ (i : ι) (hi : i ∈ S), s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
rw [biInter_eq_iInter]
ι✝ : Sort ?u.642
α : Type u_2
β : Type ?u.648
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
ι✝ : Sort ?u.642
α : Type u_2
β : Type ?u.648
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
haveI := hS.toEncodable
no goals
ι✝ : Sort ?u.642
α : Type u_2
β : Type ?u.648
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
exact countable_iInter_mem.trans Subtype.forall