epi_f_iff — Mathlib

English

In an exact short complex, f is epi if and only if g is zero.

Русский

В экзактном кратком комплексе f является эпиморфизмом тогда и только тогда, когда g равно нулю.

LaTeX

$$S\text{.Exact} \Rightarrow (\mathrm{Epi}(S.f) \iff S.g = 0)$$

Lean4

theorem epi_f_iff (hS : S.Exact) : Epi S.f ↔ S.g = 0 :=
  by
  constructor
  · intro
    rw [← cancel_epi S.f, zero, comp_zero]
  · exact hS.epi_f

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