ker_comp_of_ker_eq_bot — Mathlib

English

If ker g = ⊥, then ker(g ∘ f) = ker f; composition with a map with trivial kernel preserves the kernel of f.

Русский

Если ker g = ⊥, то ker(g ∘ f) = ker f; композиция с отображением с тривиальным ядром сохраняет ядро f.

LaTeX

$$$\ker(g \circ f) = \ker f \quad\text{если } \ker g = ⊥$$$

Lean4

theorem ker_comp_of_ker_eq_bot (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) :
    ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f := by rw [ker_comp, hg, Submodule.comap_bot]

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