hasInjectiveDimensionLT_X₃_iff — Mathlib

English

In a short exact sequence S, if X2 is Injective, then HasInjectiveDimensionLT X3 (n+1) is equivalent to HasInjectiveDimensionLT X1 (n+2).

Русский

В последовательности SE, если X2 инъективен, то LT X3 (n+1) эквивалентно LT X1 (n+2).

LaTeX

$$$S.ShortExact \land HasInjectiveDimensionLT S.X_2 1 \Rightarrow (\text{HasInjectiveDimensionLT}(S.X_3,n+1) \iff \text{HasInjectiveDimensionLT}(S.X_1,n+2))$$$

Lean4

theorem hasInjectiveDimensionLT_X₃_iff (n : ℕ) (h₂ : Injective S.X₂) :
    HasInjectiveDimensionLT S.X₃ (n + 1) ↔ HasInjectiveDimensionLT S.X₁ (n + 2) :=
  ⟨fun _ ↦ hS.hasInjectiveDimensionLT_X₁ (n + 1) inferInstance inferInstance, fun _ ↦
    hS.hasInjectiveDimensionLT_X₃ (n + 1) inferInstance inferInstance⟩

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