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 ≤ a, then Codisjoint a b.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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