hasInjectiveDimensionLT_of_ge — Mathlib

English

If n ≤ m and HasInjectiveDimensionLT X n, then HasInjectiveDimensionLT X m.

Русский

Если n ≤ m и HasInjectiveDimensionLT X n, то HasInjectiveDimensionLT X m.

LaTeX

$$$\text{HasInjectiveDimensionLT}(X,m) \text{ при } n \le m$$$

Lean4

theorem hasInjectiveDimensionLT_of_ge (m : ℕ) (h : n ≤ m) [HasInjectiveDimensionLT X n] : HasInjectiveDimensionLT X m :=
  by
  letI := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y e
  exact e.eq_zero_of_hasInjectiveDimensionLT n (by cutsat)

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