hasProjectiveDimensionLT_zero_iff_isZero

English

HasProjectiveDimensionLT X 0 if and only if X is zero.

Русский

HasProjectiveDimensionLT X 0 тогда и только тогда, когда X нулевой объект.

LaTeX

$$$ \operatorname{HasProjectiveDimensionLT}(X,0) \iff \operatorname{IsZero}(X) $$$

Lean4

theorem hasProjectiveDimensionLT_zero_iff_isZero : HasProjectiveDimensionLT X 0 ↔ IsZero X :=
  ⟨fun _ ↦ isZero_of_hasProjectiveDimensionLT_zero X, fun h ↦ h.hasProjectiveDimensionLT_zero⟩

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