isConstant_coe — Mathlib

English

If a function f is constant equal to b at every point, then its germ is constant.

Русский

Если функция f равна константе b на все точки, то её жермен константен.

LaTeX

$$$\forall f: \alpha \to \beta, \forall b, (\forall x', f(x') = b) \Rightarrow (\mathrm{Germ.ofFun}(f) \text{ isConstant}).$$$

Lean4

theorem isConstant_coe {l : Filter α} {b} (h : ∀ x', f x' = b) : (↑f : Germ l β).IsConstant :=
  ⟨b, Eventually.of_forall h⟩

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