zero_top — Mathlib

English

The square with the top morphism zero and the bottom morphism id_X is a pushout.

Русский

Квадрат сверху нулевым морфизмом, снизу — Id_X, является пушаутом.

LaTeX

$$$\operatorname{IsPushout}(0:(0\to 0),\; 0:(0\to X),\; 0:(0\to X),\; \mathrm{id}_X)$$$

Lean4

/-- The square with `0 : 0 ⟶ 0` on the top and `𝟙 X` on the bottom is a pushout square. -/
@[simp]
theorem zero_top (X : C) : IsPushout (0 : (0 : C) ⟶ 0) (0 : 0 ⟶ X) (0 : 0 ⟶ X) (𝟙 X) :=
  (zero_left X).flip

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