dual

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.dual

English

If a and b are codisjoint, then a is codisjoint with (c ⊔ b).

Русский

Если a и b кодиссоединены, то a кодиссоединено с (c ⊔ b).

LaTeX

$$$Codisjoint a b \rightarrow Codisjoint a (c \sqcup b)$$$

Lean4

theorem dual [PartialOrder α] [OrderTop α] {a b : α} : Codisjoint a b → Disjoint (toDual a) (toDual b) :=
  id

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

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

Разделы

Аффилиация

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