projectiveDimension_ge_iff — Mathlib

English

For any X, there is an equivalence between 'projectiveDimension X ≤ n' and HasProjectiveDimensionLE X n.

Русский

Для любого X существует эквивалентность между 'pd(X) ≤ n' и HasProjectiveDimensionLE X n.

LaTeX

$$$\forall X:\mathcal C, \forall n:\mathbb N,\big( \operatorname{projectiveDimension}(X) \le n \big) \iff HasProjectiveDimensionLE(X,n)$$$

Lean4

theorem projectiveDimension_ge_iff (X : C) (n : ℕ) : n ≤ projectiveDimension X ↔ ¬HasProjectiveDimensionLT X n := by
  rw [← not_iff_not, not_le, not_not, projectiveDimension_lt_iff]

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