sup_lt_of_lt_sdiff_left

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#sup_lt_of_lt_sdiff_left

← MathLib Explorer

English

If y < z \ x and x ≤ z, then x ⊔ y < z.

Русский

Если y < z \ x и x ≤ z, то x ⊔ y < z.

LaTeX

$$$$ y < z \setminus x \land x \le z \Rightarrow x \lor y < z $$$$

Lean4

theorem sup_lt_of_lt_sdiff_left (h : y < z \ x) (hxz : x ≤ z) : x ⊔ y < z :=
  by
  rw [← sup_sdiff_cancel_right hxz]
  refine (sup_le_sup_left h.le _).lt_of_not_ge fun h' => h.not_ge ?_
  rw [← sdiff_idem]
  exact (sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le

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

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

Разделы

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

Аффилиация

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