English
If a filter l has a basis {s_i} indexed by i with p i and s_i ∈ l, then the neighborhood filter 𝓝 l has basis p i with sets { l' | s_i ∈ l' }.
Русский
Если у фильтра l есть базис {s_i} индексируемый i с условиями p(i) и s_i ∈ l, то окрестности 𝓝 l имеют базис p(i) состоящий из множеств { l' : Filter α | s_i ∈ l' }.
LaTeX
$$$\text{nhds}'\ {l} {p} {s} (h : \text{HasBasis } l\ p\ s) : \text{HasBasis } (\mathcal{N} l)\ p\ (\lambda i. \{l' : \text{Filter}(\alpha) \mid s i \in l'\}).$$$
Lean4
theorem nhds' {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
HasBasis (𝓝 l) p fun i => {l' | s i ∈ l'} := by simpa only [Iic_principal] using h.nhds
