injectiveDimension_ge_iff — Mathlib

English

For any X and n, n ≤ injectiveDimension X iff not HasInjectiveDimensionLT X n.

Русский

Для любого X и n: n ≤ injDim(X) тогда и только тогда, когда HasInjectiveDimensionLT X n не выполняется.

LaTeX

$$$n \le \operatorname{injectiveDimension}(X) \iff \lnot\text{HasInjectiveDimensionLT}(X,n)$$$

Lean4

theorem injectiveDimension_ge_iff (X : C) (n : ℕ) : n ≤ injectiveDimension X ↔ ¬HasInjectiveDimensionLT X n := by
  rw [← not_iff_not, not_le, not_not, injectiveDimension_lt_iff]

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