swap

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#IsAntichain.swap

English

IsAntichain r s is equivalent to IsAntichain (swap r) s.

Русский

IsAntichain r s эквивалентно IsAntichain (swap r) s.

LaTeX

$$$IsAntichain(r,s) \Rightarrow IsAntichain(Function.swap(r), s)$$$

Lean4

theorem swap (hs : IsAntichain r s) : IsAntichain (swap r) s :=
  hs.flip

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

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

Разделы

Аффилиация

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