coe_inj — Mathlib

English

The natural map that sends a locally constant function to its underlying function is injective; in other words, locally constant maps are determined by their pointwise values: if (f : X → Y) = g for LocallyConstant X Y, then f = g.

Русский

Естественный отображение, отправляющее локально константную функцию на её значений как на функцию, инъективно; то есть локально константные отображения определяется по значениям на каждой точке: если (f : X → Y) = g, тогда f = g.

LaTeX

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

Lean4

@[norm_cast]
theorem coe_inj {f g : LocallyConstant X Y} : (f : X → Y) = g ↔ f = g :=
  coe_injective.eq_iff

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