exists_eq_const — Mathlib

English

If X is PreconnectedSpace and Y is nonempty, every LocallyConstant f: X → Y is constant; i.e., there exists y with f = const X y.

Русский

При [PreconnectedSpace X] и [Nonempty Y] любая локально константная функция f: X → Y есть константная, т.е. существует y such that f = const(X,y).

LaTeX

$$$[PreconnectedSpace X] [Nonempty Y] (f: LocallyConstant X Y) \\\\Rightarrow \\\\exists y\\\\in Y, f = const(X,y)$$$

Lean4

theorem exists_eq_const [PreconnectedSpace X] [Nonempty Y] (f : LocallyConstant X Y) : ∃ y, f = const X y :=
  by
  rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)
  · exact ⟨f x, f.eq_const x⟩
  · exact ⟨Classical.arbitrary Y, ext fun x => (hX ⟨x⟩).elim⟩

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