symmDiff_symmDiff_left — Mathlib

English

Inf distributes over symmetric difference on the right: a Δ b ∧ c = (a ∧ c) Δ (b ∧ c).

Русский

Inf распределяется над симмDiff справа: a Δ b ∧ c = (a ∧ c) Δ (b ∧ c).

LaTeX

$$a Δ b ∧ c = (a ∧ c) Δ (b ∧ c)$$

Lean4

theorem symmDiff_symmDiff_left : a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c :=
  calc
    a ∆ b ∆ c = a ∆ b \ c ⊔ c \ a ∆ b := symmDiff_def _ _
    _ = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) := by {
      rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff]
    }
    _ = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c := by ac_rfl

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