exists_open — Mathlib

English

If hf: IsLocallyConstant f, then for each x there exists an open set U with x ∈ U such that f is constant on U.

Русский

Если hf: IsLocallyConstant f, то для каждого x существует открытое множество U с x ∈ U, такое что f константна на U.

LaTeX

$$$\\exists U : Set X, \\IsOpen U \\wedge x \\in U \\wedge \\forall x' \\in U, f(x') = f(x)$$$

Lean4

theorem exists_open {f : X → Y} (hf : IsLocallyConstant f) (x : X) :
    ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x :=
  (iff_exists_open f).1 hf x

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