ker_comp — Mathlib

English

The kernel of the composition g ∘ f is the preimage via f of the kernel of g, i.e., ker(g ∘ f) = comap f (ker g).

Русский

Ядро композиции g ∘ f равно прообразу через f ядра g: ker(g ∘ f) = comap f (ker g).

LaTeX

$$$\ker(g \circ f) = \mathrm{comap} \, f (\ker g)$$$

Lean4

theorem ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = comap f (ker g) :=
  rfl

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