ext — Mathlib

English

Locally constant functions are completely determined by their values at each point: if f and g agree at every point, then f equals g.

Русский

Локально константные функции полностью определяются своими значениями в каждой точке: если f(x) = g(x) для всех x, тогда f = g.

LaTeX

$$$\\\\forall f,g:\\\\mathrm{LocallyConstant}(X,Y), (\\\\forall x, f(x)=g(x)) \\\\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext ⦃f g : LocallyConstant X Y⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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