hasProjectiveDimensionLT_X₃_iff

English

If X₂ is projective, then in a short exact sequence S, HasProjectiveDimensionLT X₃ (n+2) is equivalent to HasProjectiveDimensionLT X₁ (n+1).

Русский

Если X₂ проективен, то в короткой точной последовательности HasProjectiveDimensionLT X₃ (n+2) эквивалентна HasProjectiveDimensionLT X₁ (n+1).

LaTeX

$$$\forall S.ShortExact, \forall n:\mathbb{N}, \text{Projective}(S.X_2) \rightarrow HasProjectiveDimensionLT(S.X_3, n+2) \leftrightarrow HasProjectiveDimensionLT(S.X_1, n+1)$$$

Lean4

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

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