iff_exists_open — Mathlib

English

IsLocallyConstant f holds if and only if there exists, for every x, an open neighborhood U of x such that f is constant on U.

Русский

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

LaTeX

$$$\\IsLocallyConstant(f) \\iff \\forall x, \\exists U, \\IsOpen(U) \\wedge x \\in U \\wedge \\forall x' \\in U, f(x') = f(x)$$$

Lean4

theorem iff_exists_open (f : X → Y) : IsLocallyConstant f ↔ ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x :=
  (IsLocallyConstant.tfae f).out 0 4

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