symmDiff_eq_sup — Mathlib

English

The biconditional between symmetric difference and join equals disjointness: symmDiff a b equals a ⊔ b if and only if a and b are disjoint.

Русский

Грубая эквивалентность между симмDiff и объединением: symmDiff a b = a ⊔ b тогда и только тогда, когда a и b несовместны.

LaTeX

$$symmDiff a b = a ⊔ b ↔ Disjoint a b$$

Lean4

theorem symmDiff_eq_sup : a ∆ b = a ⊔ b ↔ Disjoint a b :=
  by
  refine ⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩
  rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h
  exact h.of_disjoint_inf_of_le le_sup_left

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