nhds_eq' — Mathlib

English

A variant of nhds_eq with a set-valued predicate; the neighborhood filter equals a lift by mapping s to {ℓ'| s ∈ ℓ'}.

Русский

Вариант nhds_eq с множеством условий; окрестности равны подъёму, отображающему s в {ℓ' | s ∈ ℓ'}.

LaTeX

$$$$\mathcal{N}(l)=l.lift'(\{s:\! Set\;\text{of } l'\;|\; s\in l'\}).$$$$

Lean4

theorem nhds_eq' (l : Filter α) : 𝓝 l = l.lift' fun s => {l' | s ∈ l'} := by
  simpa only [Function.comp_def, Iic_principal] using nhds_eq l

Похожие утверждения