ext_of_isTriangulatedClosed₃ — Mathlib

English

Similar closure properties extend to the third component of triangles, ensuring that if P holds for two consecutive components, a corresponding third component closure also holds under distinguished triangles.

Русский

Подобные свойства замыкания распространяются на третью компоненту треугольников: если P выполняется на двух последовательных компонентах, тогда замыкание соответствующего третьего компонента сохраняется для выделенных треугольников.

LaTeX

$$$[P.IsTriangulatedClosed₃]$ ensures closure for the third vertex given the first two, under distTriang.$$

Lean4

theorem ext_of_isTriangulatedClosed₃ [P.IsTriangulatedClosed₃] [P.IsClosedUnderIsomorphisms] (T : Triangle C)
    (hT : T ∈ distTriang C) (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P T.obj₃ := by
  simpa only [isoClosure_eq_self] using P.ext_of_isTriangulatedClosed₃' T hT h₁ h₂

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