sdiff_unique — Mathlib

English

For hz : z ≤ y and hx : x ≤ y, x ≤ z if and only if y = z ⊔ (y \ x).

Русский

Пусть z ≤ y и x ≤ y. Тогда x ≤ z тогда и только тогда, когда y = z ⊔ (y \ x).

LaTeX

$$$(hz : z \le y) (hx : x \le y) : x \le z \iff y = z \sqcup (y \setminus x)$$$

Lean4

protected theorem sdiff_unique (hd : Disjoint x z) (hz : z ≤ y) (hs : y ≤ x ⊔ z) : y \ x = z :=
  sdiff_unique
    (by
      rw [← inf_eq_right] at hs
      rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z, hs, sup_eq_left])
    (by rw [inf_assoc, hd.eq_bot, inf_bot_eq])
      -- cf. `IsCompl.disjoint_left_iff` and `IsCompl.disjoint_right_iff`

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