comp_ι_eq — Mathlib

English

The kernel of f, regarded as a subset of V1, equals the image of the kernel under the natural embedding.

Русский

Ядро отображения f, рассматриваемое как подмножество V1, совпадает с образом ядра при естественном вложении.

LaTeX

$$$(f.ker : Set V_1) = (f : V_1 \\to V_2)^{-1} \\{0\\}$$$

Lean4

theorem comp_ι_eq : f.comp (ι f g) = g.comp (ι f g) := by
  ext x
  rw [comp_apply, comp_apply, ← sub_eq_zero, ← NormedAddGroupHom.sub_apply]
  exact x.2

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