le_sup_right_iff_inf_left_le

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#IsCompl.le_sup_right_iff_inf_left_le

← MathLib Explorer

English

Given h is a complement, a ≤ b ⊔ y is equivalent to a ⊓ x ≤ b.

Русский

Пусть h — комплемент; тогда a ≤ b ⊔ y эквивалентно a ⊓ x ≤ b.

LaTeX

$$$$ IsCompl(x,y) \rightarrow (a \le b \vee y) \Leftrightarrow (a \wedge x \le b). $$$$

Lean4

theorem le_sup_right_iff_inf_left_le {a b} (h : IsCompl x y) : a ≤ b ⊔ y ↔ a ⊓ x ≤ b :=
  ⟨h.inf_left_le_of_le_sup_right, h.symm.dual.inf_left_le_of_le_sup_right⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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