instHasProjectiveDimensionLTSucc — Mathlib

English

An instance giving HasProjectiveDimensionLT X (n+1) from HasProjectiveDimensionLT X n using the standard construction.

Русский

Инстанс порождает HasProjectiveDimensionLT X (n+1) из HasProjectiveDimensionLT X n через стандартную конструкцию.

LaTeX

$$$ [HasProjectiveDimensionLT X n] : HasProjectiveDimensionLT X (n+1) $$$

Lean4

instance [HasProjectiveDimensionLT X n] : HasProjectiveDimensionLT X n.succ :=
  inferInstanceAs (HasProjectiveDimensionLT X (n + 1))

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