comp_inj — Mathlib

English

For an embedding h: N ↪[L] P, the map f ↦ h.comp f is injective on embeddings M ↪[L] N.

Русский

Для вложения h: N ↪[L] P отображение f ↦ h.comp f инъективно на множествах вложений M ↪[L] N.

LaTeX

$$$(h:\\, N \\hookrightarrow_L P).comp\\, f = (h:\\, N \\hookrightarrow_L P).comp\\, g \\Leftrightarrow f = g$$$

Lean4

@[simp]
theorem comp_inj (h : N ↪[L] P) (f g : M ↪[L] N) : h.comp f = h.comp g ↔ f = g :=
  ⟨fun eq ↦ h.comp_injective eq, congr_arg h.comp⟩

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