coe_injective — Mathlib

English

The coercion from embeddings to functions is injective; if two embeddings have the same underlying function, they are equal.

Русский

Коэрция из вложений в функции инъективна: если два вложения имеют одинаковую опорную функцию, они равны.

LaTeX

$$$\\text{Injective} \\; (\\,↑\\,): (M \\hookrightarrow_L N) \\to (M \\to N)$$$

Lean4

theorem coe_injective : @Function.Injective (M ↪[L] N) (M → N) (↑)
  | f, g, h => by
    cases f
    cases g
    congr
    ext x
    exact funext_iff.1 h x

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