isRotated_comm — Mathlib

English

The rotation relation is symmetric in both directions, i.e., l is a rotation of l' iff l' is a rotation of l.

Русский

Отношение вращения симметрично: l вращается относительно l' тогда и только тогда, когда l' вращается относительно l.

LaTeX

$$$ l \sim_{\mathrm{rot}} l' \iff l' \sim_{\mathrm{rot}} l $$$

Lean4

theorem isRotated_comm : l ~r l' ↔ l' ~r l :=
  ⟨IsRotated.symm, IsRotated.symm⟩

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