disjoint_sdiff_iff_le — Mathlib

English

Under hz : z ≤ y and hx : x ≤ y, Disjoint z (y \ x) if and only if z ≤ x.

Русский

При условии z ≤ y и x ≤ y, Disjoint z (y \ x) эквивалентно z ≤ x.

LaTeX

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

Lean4

theorem disjoint_sdiff_iff_le (hz : z ≤ y) (hx : x ≤ y) : Disjoint z (y \ x) ↔ z ≤ x :=
  ⟨fun H =>
    le_of_inf_le_sup_le (le_trans H.le_bot bot_le)
      (by
        rw [sup_sdiff_cancel_right hx]
        grw [sdiff_le]
        rw [sup_eq_right.2 hz]),
    fun H => disjoint_sdiff_self_right.mono_left H⟩
    -- cf. `IsCompl.le_left_iff` and `IsCompl.le_right_iff`

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