left_le_of_le_inf_right

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.left_le_of_le_inf_right

English

If a ∧ b ≤ c and Codisjoint b c, then a ≤ c.

Русский

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

LaTeX

$$$a \wedge b \le c \;\land\; Codisjoint b c \rightarrow a \le c$$$

Lean4

theorem left_le_of_le_inf_right (h : a ⊓ b ≤ c) (hd : Codisjoint b c) : a ≤ c :=
  @Disjoint.left_le_of_le_sup_right αᵒᵈ _ _ _ _ _ h hd.symm

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

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

Разделы

Аффилиация

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