α : Type u_1
β : Type ?u.15651
γ : Type ?u.15654
ι : Sort ?u.15657
ι' : Sort ?u.15660
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
⊢ IsBasis.filter (_ : IsBasis (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t) = FilterBasis.filter (FilterBasis.ofSets s)
α : Type u_1
β : Type ?u.15651
γ : Type ?u.15654
ι : Sort ?u.15657
ι' : Sort ?u.15660
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
⊢ generate s = generate (sInter '' {t | Set.Finite t ∧ t ⊆ s})
rw [← FilterBasis.ofSets_sets, FilterBasis.generate, ← (hasBasis_generate s).filter_eq]
no goals
α : Type u_1
β : Type ?u.15651
γ : Type ?u.15654
ι : Sort ?u.15657
ι' : Sort ?u.15660
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
⊢ IsBasis.filter (_ : IsBasis (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t) = FilterBasis.filter (FilterBasis.ofSets s)
rfl