iff_is_const — Mathlib

English

For [PreconnectedSpace X], IsLocallyConstant f iff ∀ x y, f x = f y.

Русский

Для [PreconnectedSpace X] локально константность эквивалентна тому, что для всех x,y выполняется f x = f y.

LaTeX

$$[PreconnectedSpace X] {f : X → Y} IsLocallyConstant f ↔ ∀ x y, f x = f y$$

Lean4

theorem iff_is_const [PreconnectedSpace X] {f : X → Y} : IsLocallyConstant f ↔ ∀ x y, f x = f y :=
  ⟨fun h _ _ => h.apply_eq_of_isPreconnected isPreconnected_univ trivial trivial, of_constant _⟩

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