iff_eventually_eq — Mathlib

English

IsLocallyConstant f is equivalent to the property that for every x, eventually near x we have f(y) = f(x).

Русский

IsLocallyConstant f эквивалентна тому, что для каждого x верно, что в окрестности x существует окрестность, на которой значения функции совпадают с f(x).

LaTeX

$$$\\IsLocallyConstant(f) \\iff ∀ x, ∀^\\! y \\text{ in } 𝓝(x), f(y) = f(x)$$$

Lean4

theorem iff_eventually_eq (f : X → Y) : IsLocallyConstant f ↔ ∀ x, ∀ᶠ y in 𝓝 x, f y = f x :=
  (IsLocallyConstant.tfae f).out 0 1

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