eq_const — Mathlib

English

For a [PreconnectedSpace X], a locally constant f: X → Y is constant with value f(x) on all of X.

Русский

Для [PreconnectedSpace X] локально константная f: X → Y равна константе на X со значением f(x).

LaTeX

$$$[PreconnectedSpace X] {f : X → Y} (hf : IsLocallyConstant f) (x : X), f = \text{const}_X (f x)$$$

Lean4

theorem eq_const [PreconnectedSpace X] {f : X → Y} (hf : IsLocallyConstant f) (x : X) : f = Function.const X (f x) :=
  funext fun y => hf.apply_eq_of_preconnectedSpace y x

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