sdiff_eq_left — Mathlib

English

If x and z are disjoint and y = x ⊔ z, then y \ x = z.

Русский

Если x и z независимы, и y = x ⊔ z, то y \ x = z.

LaTeX

$$$\text{Disjoint } x z \rightarrow y = x \oplus z \Rightarrow y \setminus x = z$$$

Lean4

@[simp]
theorem sdiff_eq_left : x \ y = x ↔ Disjoint x y :=
  ⟨fun h ↦ disjoint_sdiff_self_left.mono_left h.ge, Disjoint.sdiff_eq_left⟩
    /- TODO: we could make an alternative constructor for `GeneralizedBooleanAlgebra` using
    `Disjoint x (y \ x)` and `x ⊔ (y \ x) = y` as axioms. -/

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