isIso_δ — Mathlib

English

If both ends of δ are zero in S, then δ is an isomorphism.

Русский

Если оба конца δ в S равны нулю, то δ — изоморфизм.

LaTeX

$$$$ \operatorname{IsZero}(S.L_0.X_2) \land \operatorname{IsZero}(S.L_3.X_2) \Rightarrow \operatorname{IsIso}(S.\delta) $$$$

Lean4

theorem isIso_δ (h₀ : IsZero S.L₀.X₂) (h₃ : IsZero S.L₃.X₂) : IsIso S.δ :=
  @Balanced.isIso_of_mono_of_epi _ _ _ _ _ S.δ (S.mono_δ h₀) (S.epi_δ h₃)

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