eq_of_germ_isConstant — Mathlib

English

If X is preconnected and each germ (f at x) is constant, then f is constant on X.

Русский

Если X является предсоединённым пространством и каждый гёрм функции f константен, то f константна на X.

LaTeX

$$$[i : \text{PreconnectedSpace } X]\; (\forall x, (f : \mathrm{Germ}(\mathcal N x) Y).IsConstant) \Rightarrow \forall x, x', f x = f x'$$$

Lean4

theorem eq_of_germ_isConstant [i : PreconnectedSpace X] (h : ∀ x : X, (f : Germ (𝓝 x) Y).IsConstant) (x x' : X) :
    f x = f x' :=
  (IsLocallyConstant.of_germ_isConstant h).apply_eq_of_isPreconnected (preconnectedSpace_iff_univ.mp i) (by trivial)
    (by trivial)

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