comp_injective — Mathlib

English

If f,g are exact, g' is injective and sends 0 to 0, then f and g'∘g are exact.

Русский

Если f,g точные, g' инъективна и сохраняет 0, то f и g'∘g точные.

LaTeX

$$$\\text{Exact}(f,g) \\land \\text{Injective}(g') \\land g'(0)=0 \\Rightarrow \\text{Exact}(f,\\; g'\\circ g)$$$

Lean4

theorem comp_injective [Zero P] [Zero P'] (exact : Exact f g) (inj : Function.Injective g') (h0 : g' 0 = 0) :
    Exact f (g' ∘ g) := by
  intro x
  refine ⟨fun H => exact x |>.mp <| inj <| h0 ▸ H, ?_⟩
  intro H
  rw [Function.comp_apply, exact x |>.mpr H, h0]

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