α : Type u_1
β : Type ?u.68520
γ : Type ?u.68523
ι : Sort u_2
ι' : Sort ?u.68529
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
⊢ (⋂ (i : Set α) (_ : i ∈ l.sets), i) = ⋂ (i : ι) (_ : p i), s i
α : Type u_1
β : Type ?u.68520
γ : Type ?u.68523
ι : Sort u_2
ι' : Sort ?u.68529
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
⊢ ⋂₀ l.sets = ⋂ (i : ι) (_ : p i), s i
rw [sInter_eq_biInter]
no goals
α : Type u_1
β : Type ?u.68520
γ : Type ?u.68523
ι : Sort u_2
ι' : Sort ?u.68529
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
⊢ (⋂ (i : Set α) (_ : i ∈ l.sets), i) = ⋂ (i : ι) (_ : p i), s i
exact h.biInter_mem monotone_id