disjoint_compl_right

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#LE.le.disjoint_compl_right

English

If a ≤ b then Disjoint a bᶜ.

Русский

Если a ≤ b, то Disjoint a bᶜ.

LaTeX

$$$ a \\le b \\Rightarrow Disjoint a b^{\\complement} $$$

Lean4

theorem disjoint_compl_right (h : a ≤ b) : Disjoint a bᶜ :=
  _root_.disjoint_compl_right.mono_left h

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

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

Разделы

Аффилиация

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