hasProjectiveDimensionLT_of_ge — Mathlib

English

If HasProjectiveDimensionLT X n holds and m ≥ n, then HasProjectiveDimensionLT X m holds.

Русский

Если HasProjectiveDimensionLT X n, и m ≥ n, то HasProjectiveDimensionLT X m.

LaTeX

$$$ \forall m\ge n,\ HasProjectiveDimensionLT(X,n) \Rightarrow HasProjectiveDimensionLT(X,m) $$$

Lean4

theorem hasProjectiveDimensionLT_of_ge (m : ℕ) (h : n ≤ m) [HasProjectiveDimensionLT X n] :
    HasProjectiveDimensionLT X m := by
  letI := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  intro i hi Y e
  exact e.eq_zero_of_hasProjectiveDimensionLT n (by cutsat)

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