exists_eq_const — Mathlib

English

If X is nonempty and Y is nonempty, a locally constant f: X → Y is constant on X; hence f = const X (f arbitrary value).

Русский

Если X непусто, то локально константная функция f: X → Y равна константе на X.

LaTeX

$$$[PreconnectedSpace X] [Nonempty Y] {f : X → Y} IsLocallyConstant f → ∃ y, f = const_X y$$$

Lean4

theorem exists_eq_const [PreconnectedSpace X] [Nonempty Y] {f : X → Y} (hf : IsLocallyConstant f) :
    ∃ y, f = Function.const X y := by
  rcases isEmpty_or_nonempty X with h | h
  · exact ⟨Classical.arbitrary Y, funext <| h.elim⟩
  · exact ⟨f (Classical.arbitrary X), hf.eq_const _⟩

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