apply_eq_of_preconnectedSpace — Mathlib

English

If X is PreconnectedSpace, then every locally constant map f: X → Y is constant on X: f(x)=f(y) for all x,y.

Русский

Если X — предсоединенное пространство, то любая локально константная карта f: X → Y константна на X.

LaTeX

$$$[PreconnectedSpace X] (f: LocallyConstant X Y) \\Rightarrow \\forall x,y, f(x)=f(y)$$$

Lean4

theorem apply_eq_of_preconnectedSpace [PreconnectedSpace X] (f : LocallyConstant X Y) (x y : X) : f x = f y :=
  f.isLocallyConstant.apply_eq_of_isPreconnected isPreconnected_univ trivial trivial

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