sup_left

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Disjoint.sup_left

English

If Disjoint a c and Disjoint b c, then Disjoint (a ⊔ b) c.

Русский

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

LaTeX

$$Disjoint a c → Disjoint b c → Disjoint (a ⊔ b) c$$

Lean4

theorem sup_left (ha : Disjoint a c) (hb : Disjoint b c) : Disjoint (a ⊔ b) c :=
  disjoint_sup_left.2 ⟨ha, hb⟩

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

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

Разделы

Аффилиация

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