toHom_inj — Mathlib

English

Two embeddings are equal if and only if their associated L-homomorphisms are equal.

Русский

Два вложения равны тогда и только тогда, когда равны их соответствующие L-гомоморфизмы.

LaTeX

$$$f.toHom = g.toHom \\;\\Leftrightarrow\\; f = g$$$

Lean4

@[simp]
theorem toHom_inj {f g : M ↪[L] N} : f.toHom = g.toHom ↔ f = g :=
  ⟨fun h ↦ toHom_injective h, fun h ↦ congr_arg (·.toHom) h⟩

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