nhds — Mathlib

English

There is a compatible FTCFilter structure on the neighborhood filter at a; i.e., nhds a participates in FTCFilter with itself.

Русский

Окрестности точки a участвуют в FTCFilter как совместимая структура с самой собой.

LaTeX

$$$\\mathrm{FTCFilter}(a, \\mathcal{N}(a), \\mathcal{N}(a))$$$

Lean4

instance nhds (a : ℝ) : FTCFilter a (𝓝 a) (𝓝 a)
    where
  pure_le := pure_le_nhds a
  le_nhds := le_rfl

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