instHasInjectiveDimensionLTHAddNat

English

If HasInjectiveDimensionLT X n holds, then for any k, HasInjectiveDimensionLT X (n + k) also holds.

Русский

Если выполнено HasInjectiveDimensionLT X n, то при любом k также выполняется HasInjectiveDimensionLT X (n + k).

LaTeX

$$$\forall k:\; \text{HasInjectiveDimensionLT}(X, n+k)$, если $\text{HasInjectiveDimensionLT}(X,n)$$$

Lean4

instance [HasInjectiveDimensionLT X n] (k : ℕ) : HasInjectiveDimensionLT X (n + k) :=
  hasInjectiveDimensionLT_of_ge X n (n + k) (by cutsat)

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