le_compl_iff_disjoint_right

Mathlib.Order.Heyting.Basic

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

English

a ≤ bᶜ iff a is disjoint from b.

Русский

a ≤ bᶜ эквивалентно тому, что a и b попадают в дизъюнктность (Disjoint).

LaTeX

$$$ a \\le b^{\\complement} \\iff \\text{Disjoint } a\, b $$$

Lean4

theorem le_compl_iff_disjoint_right : a ≤ bᶜ ↔ Disjoint a b := by rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]

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

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

Разделы

Аффилиация

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