sup_lt_of_lt_sdiff_right — Mathlib

English

Let α be a generalized Boolean algebra. If x < z \\ y and y ≤ z, then x ⊔ y < z.

Русский

Пусть α — обобщённая булева алгебра. Пусть x < z \ y и y ≤ z, тогда x ⊔ y < z.

LaTeX

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

Lean4

theorem sup_lt_of_lt_sdiff_right (h : x < z \ y) (hyz : y ≤ z) : x ⊔ y < z :=
  by
  rw [← sdiff_sup_cancel hyz]
  refine lt_of_le_not_ge (by grw [h]) fun h' => h.not_ge ?_
  rw [← sdiff_idem]
  exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le

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