swap_lt_swap_iff

Mathlib.Order.Concept

URI: https://scilib.ai/kg/mathlib#Concept.swap_lt_swap_iff

English

For two concepts c and d, c.swap < d.swap if and only if d < c. The swap operation preserves strict order reversal.

Русский

Для концептов c и d: c.swap < d.swap тогда и только тогда, когда d < c.

LaTeX

$$$$ c.swap < d.swap \;\iff\; d < c. $$$$

Lean4

@[simp]
theorem swap_lt_swap_iff : c.swap < d.swap ↔ d < c :=
  intent_ssubset_intent_iff

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

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

Разделы

Аффилиация

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