of_codisjoint_sup_of_le'

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.of_codisjoint_sup_of_le'

English

If Codisjoint (a ⊔ b) c and c ≤ b, then Codisjoint a b.

Русский

Если Codisjoint (a ⊔ b) c и c ≤ b, тогда Codisjoint a b.

LaTeX

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

Lean4

theorem of_codisjoint_sup_of_le' (h : Codisjoint (a ⊔ b) c) (hle : c ≤ b) : Codisjoint a b :=
  @Disjoint.of_disjoint_inf_of_le' αᵒᵈ _ _ _ _ _ h hle

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

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

Разделы

Аффилиация

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