codisjoint_toDual_iff

Mathlib.Order.Disjoint

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

English

The codisjoint relation commutes with duality: codisjoint (toDual a) (toDual b) holds exactly when codisjoint a b holds.

Русский

Кодиссоединение (toDual a) (toDual b) эквивалентно кодиссоединению a b.

LaTeX

$$$Codisjoint (toDual a) (toDual b) \iff Codisjoint a b$$$

Lean4

@[simp]
theorem codisjoint_toDual_iff [PartialOrder α] [OrderBot α] {a b : α} :
    Codisjoint (toDual a) (toDual b) ↔ Disjoint a b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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