injectiveDimension_eq_bot_iff — Mathlib

English

Injective dimension equals bottom if and only if the object is zero (IsZero).

Русский

Инъективная размерность равна нижнему пределу тогда и только тогда, когда объект нулевой.

LaTeX

$$$ \operatorname{injectiveDimension}(X) = \bot \iff \text{IsZero}(X) $$$

Lean4

theorem injectiveDimension_eq_bot_iff (X : C) : injectiveDimension X = ⊥ ↔ Limits.IsZero X := by
  rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff, Nat.cast_zero, ← WithBot.lt_coe_bot,
    bot_eq_zero', WithBot.coe_zero]

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