left_le_of_le_inf_left

Mathlib.Order.Disjoint

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

English

If a ∧ b ≤ c and Codisjoint b c, then a ≤ c (dual statement to the previous).

Русский

Если a ∧ b ≤ c и Codisjoint b c, тогда a ≤ c (дубль предыдущего).

LaTeX

$$$\operatorname{INF}(a,b) \le c \land Codisjoint b c \rightarrow a \le c$$$

Lean4

theorem left_le_of_le_inf_left (h : b ⊓ a ≤ c) (hd : Codisjoint b c) : a ≤ c :=
  hd.left_le_of_le_inf_right <| by rwa [inf_comm]

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

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

Разделы

Аффилиация

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