English
From an indexed family of sets (s i) with an IsBasis property, one constructs a FilterBasis consisting of all sets that are exactly some s i.
Русский
Из индексированной семейства множеств (s_i) с свойством IsBasis строится FilterBasis, состоящий из всех множеств, совпадающих с некоторым s_i.
LaTeX
$$$\mathrm{sets}(\mathrm{filterBasis}(h)) = \{ t \mid \exists i,\ p(i) \wedge s(i)=t \}. $$$
Lean4
/-- Constructs a filter basis from an indexed family of sets satisfying `IsBasis`. -/
protected def filterBasis {p : ι → Prop} {s : ι → Set α} (h : IsBasis p s) : FilterBasis α
where
sets := {t | ∃ i, p i ∧ s i = t}
nonempty :=
let ⟨i, hi⟩ := h.nonempty
⟨s i, ⟨i, hi, rfl⟩⟩
inter_sets := by
rintro _ _ ⟨i, hi, rfl⟩ ⟨j, hj, rfl⟩
rcases h.inter hi hj with ⟨k, hk, hk'⟩
exact ⟨_, ⟨k, hk, rfl⟩, hk'⟩
