nhdsIcc — Mathlib

English

There is a FTCFilter around x for any x in Icc(a,b); i.e., the filter nhdsWithin x on Icc(a,b) to nhdsWithin x on Icc(a,b) exists.

Русский

Для каждого x ∈ Icc(a,b) существует FTCFilter вокруг x внутри Icc(a,b).

LaTeX

$$$\\forall x \\in \\mathrm{Icc}(a,b),\\; \\mathrm{FTCFilter}\\, x\\, (\\mathrm{nhdsWithin}\\, x\\, \\mathrm{Icc}(a,b))\\; (\\mathrm{nhdsWithin}\\, x\\, \\mathrm{Icc}(a,b))$$$

Lean4

instance nhdsIcc {x a b : ℝ} [h : Fact (x ∈ Icc a b)] : FTCFilter x (𝓝[Icc a b] x) (𝓝[Icc a b] x)
    where
  pure_le := pure_le_nhdsWithin h.out
  le_nhds := inf_le_left

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