hasInjectiveDimensionLT_of_iso — Mathlib

English

If X ≅ X' then HasInjectiveDimensionLT X n implies HasInjectiveDimensionLT X' n.

Русский

Если X изоморфно X', то LT задержка сохраняется: HasInjectiveDimensionLT(X,n) ⇒ HasInjectiveDimensionLT(X',n).

LaTeX

$$$e:\, X \cong X'\Rightarrow \text{HasInjectiveDimensionLT}(X,n) \Rightarrow \text{HasInjectiveDimensionLT}(X',n)$$$

Lean4

theorem hasInjectiveDimensionLT_of_iso {X X' : C} (e : X ≅ X') (n : ℕ) [HasInjectiveDimensionLT X n] :
    HasInjectiveDimensionLT X' n :=
  e.symm.retract.hasInjectiveDimensionLT n

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