inv_rot_of_distTriang — Mathlib

English

The inverse-rotated triangle of a distinguished triangle remains distinguished after applying the opposite functor.

Русский

Обратное вращение выделенного треугольника сохраняет выделенность после применения противоположного функторa.

LaTeX

$$inv_rot_of_distTriang$$

Lean4

/-- Given any distinguished triangle `T`, then we know `T.inv_rotate` is also distinguished.
-/
theorem inv_rot_of_distTriang (T : Triangle C) (H : T ∈ distTriang C) : T.invRotate ∈ distTriang C :=
  (rotate_distinguished_triangle T.invRotate).mpr
    (isomorphic_distinguished T H T.invRotate.rotate (invRotCompRot.app T))

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