left_le_of_le_sup_left

Mathlib.Order.Disjoint

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

English

If a ≤ b, then codisjoint a c implies codisjoint b c.

Русский

Если a ≤ b, то Codisjoint a c и Codisjoint b c совместны между собой.

LaTeX

$$$a \le b \to \operatorname{Codisjoint}(a,c) \to \operatorname{Codisjoint}(b,c)$$$

Lean4

theorem left_le_of_le_sup_left (h : a ≤ c ⊔ b) (hd : Disjoint a c) : a ≤ b :=
  hd.left_le_of_le_sup_right <| by rwa [sup_comm]

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

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

Разделы

Аффилиация

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