sdiff_lt_sdiff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sdiff_lt_sdiff_right (h : x < y) (hz : z ≤ x) : x \ z < y \ z :=
  (sdiff_le_sdiff_right h.le).lt_of_not_ge fun h' => h.not_ge <| le_sdiff_sup.trans <| sup_le_of_le_sdiff_right h' hz

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