instHasInjectiveDimensionLTSucc — Mathlib

English

Let X be an object in an abelian category. If HasInjectiveDimensionLT X n holds, then HasInjectiveDimensionLT X (n+1) also holds.

Русский

Пусть X — объект абелевой категории. Если выполняется HasInjectiveDimensionLT X n, то также выполняется HasInjectiveDimensionLT X (n+1).

LaTeX

$$$\text{HasInjectiveDimensionLT}(X,n) \implies \text{HasInjectiveDimensionLT}(X,n+1)$$$

Lean4

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

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