reverse_reverse

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.reverse_reverse

English

Reverse of a RelSeries, reversed again, gives back the original RelSeries.

Русский

Обратная последовательность относительно r, которая повторно развёрнута, возвращает исходную RelSeries.

LaTeX

$$$ p.reverse.reverse = p $$$

Lean4

@[simp]
theorem reverse_reverse {r : SetRel α α} (p : RelSeries r) : p.reverse.reverse = p := by ext <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru