nhdsUniv — Mathlib

English

There is a FTCFilter relation between a real number a and the neighborhood filter restricted to univ; i.e., nhds[a] coincides with nhds within univ.

Русский

Существует отношение FTCFilter между a и окрестностями при ограничении до единого множества (univ).

LaTeX

$$$\\mathrm{FTCFilter}(a, \\mathcal{N}_{[univ]}(a), \\mathcal{N}_{[univ]}(a))$$$

Lean4

instance nhdsUniv (a : ℝ) : FTCFilter a (𝓝[univ] a) (𝓝 a) := by rw [nhdsWithin_univ]; infer_instance

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