symmDiff_sdiff_left — Mathlib

English

Symmetric difference with itself minus the first argument equals the second minus the first: a Δ (b \\ a) = b \\ a.

Русский

Симметрическая разность с разностью самого себе минус первый аргумент: a Δ (b \\ a) = b \\ a.

LaTeX

$$∀ a b, a ∆ b \\ a = b \\ a$$

Lean4

@[simp]
theorem symmDiff_sdiff_left : a ∆ b \ a = b \ a := by
  rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]

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