instHasProjectiveDimensionLTHAddNat

English

If X has HasProjectiveDimensionLT X n, then for any k, HasProjectiveDimensionLT X (n+k).

Русский

Если у X есть HasProjectiveDimensionLT X n, то для любого k имеет место HasProjectiveDimensionLT X (n+k).

LaTeX

$$$ [\text{HasProjectiveDimensionLT } X n] \Rightarrow [\text{HasProjectiveDimensionLT } X (n+k)]. $$$

Lean4

instance [HasProjectiveDimensionLT X n] (k : ℕ) : HasProjectiveDimensionLT X (n + k) :=
  hasProjectiveDimensionLT_of_ge X n (n + k) (by cutsat)

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