prop_of_isZero — Mathlib

English

If P.ContainsZero and P.IsClosedUnderIsomorphisms, then every zero object Z satisfies P Z.

Русский

Если P.ContainsZero и P.IsClosedUnderIsomorphisms, то каждый нулевой объект Z удовлетворяет P(Z).

LaTeX

$$$$ \text{If } [P.ContainsZero] \text{ and } [P.IsClosedUnderIsomorphisms], \ IsZero(Z) \Rightarrow P(Z). $$$$

Lean4

theorem prop_of_isZero [P.ContainsZero] [P.IsClosedUnderIsomorphisms] {Z : C} (hZ : IsZero Z) : P Z :=
  by
  obtain ⟨Z₀, hZ₀, h₀⟩ := P.exists_prop_of_containsZero
  exact P.prop_of_iso (hZ₀.iso hZ) h₀

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