rot_of_distTriang — Mathlib

English

If T is distinguished, then any rotation of T is also distinguished.

Русский

Если T — выделенный, то любая вращенная версия T также является выделенной.

LaTeX

$$rot_of_distTriang$$

Lean4

/-- Given any distinguished triangle `T`, then we know `T.rotate` is also distinguished.
-/
theorem rot_of_distTriang (T : Triangle C) (H : T ∈ distTriang C) : T.rotate ∈ distTriang C :=
  (rotate_distinguished_triangle T).mp H

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