nhdsUIcc — Mathlib

English

There is a FTCFilter around x for x ∈ uIcc(a,b), i.e., the uIcc-variant of the interval has a compatible FTCFilter.

Русский

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

LaTeX

$$$\\forall x\\,\\big(x \\in \\mathrm{uIcc}(a,b)\\big) \\Rightarrow \\mathrm{FTCFilter}\\, x\\, (\\mathrm{nhdsWithin}\\, x\\, \\mathrm{uIcc}(a,b))\\, (\\mathrm{nhdsWithin}\\, x\\, \\mathrm{uIcc}(a,b))$$$

Lean4

instance nhdsUIcc {x a b : ℝ} [h : Fact (x ∈ [[a, b]])] : FTCFilter x (𝓝[[[a, b]]] x) (𝓝[[[a, b]]] x) :=
  .nhdsIcc (h := h)

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