isCompl_comm

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#isCompl_comm

English

IsCompl is symmetric (again).

Русский

IsCompl симметрично (повтор).

LaTeX

$$IsCompl x y → IsCompl y x$$

Lean4

theorem _root_.isCompl_comm : IsCompl x y ↔ IsCompl y x :=
  ⟨IsCompl.symm, IsCompl.symm⟩

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

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

Разделы

Аффилиация

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