coe_injective — Mathlib

English

The coercion map from locallyFinsuppWithin U Y to X → Y is injective; two elements with equal pointwise values are the same.

Русский

Коэрция из locallyFinsuppWithin в X → Y инъективна; если значения совпадают по точкам, функции равны.

LaTeX

$$$\\text{Injective} (\\cdot : \\text{locallyFinsuppWithin } U Y \\to X \\to Y)$$$

Lean4

theorem coe_injective [Zero Y] : Injective (· : locallyFinsuppWithin U Y → X → Y) :=
  DFunLike.coe_injective

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