nhdsLeft — Mathlib

English

There is a FTCFilter around a using the left-hand endpoint, i.e., nhdsWithin (≤) a forms an FTCFilter to itself.

Русский

Существует FTCFilter вокруг точки a с левой границей, т.е. nhdsWithin (≤) a образует FTCFilter с собой.

LaTeX

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

Lean4

instance nhdsLeft (a : ℝ) : FTCFilter a (𝓝[≤] a) (𝓝[≤] a)
    where
  pure_le := pure_le_nhdsWithin right_mem_Iic
  le_nhds := inf_le_left

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