zero_bot — Mathlib

English

The square with the bottom morphisms zero and the top-left identity is a pushout.

Русский

Квадрат с нижними стрелками нулевые и верхней левой стрелкой тождество образуют пушаут.

LaTeX

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

Lean4

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

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