le_sdiff — Mathlib

English

For all x,y,z, x ≤ y \ z if and only if x ≤ y and x is disjoint from z.

Русский

Для всех x,y,z: x ≤ y \ z эквивалентно x ≤ y и x непересекается с z.

LaTeX

$$$x \le y \setminus z \iff (x \le y) \land Disjoint x z$$

Lean4

theorem le_sdiff : x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z :=
  ⟨fun h ↦ ⟨h.trans sdiff_le, disjoint_sdiff_self_left.mono_left h⟩, fun h ↦ by rw [← h.2.sdiff_eq_left];
    exact sdiff_le_sdiff_right h.1⟩

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