English
The left associativity of symmetric difference with a third argument gives a decomposition in terms of pairwise interactions: a Δ (b Δ c) = a \\ (b ⊔ c) ⊔ b \\ (a ⊔ c) ⊔ c \\ (a ⊔ b) ⊔ a ∧ b ∧ c.
Русский
Левая ассоциативность симмDiff с третьим аргументом даёт разложение по попарным взаимодействиям: a Δ (b Δ c) = …
LaTeX
$$∀ a b c, a ∆ b ∆ c = a \\ (b ⊔ c) ⊔ b \\ (a ⊔ c) ⊔ c \\ (a ⊔ b) ⊔ a ∧ b ∧ c$$
Lean4
theorem symmDiff_symmDiff_right : a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c :=
calc
a ∆ (b ∆ c) = a \ b ∆ c ⊔ b ∆ c \ a := symmDiff_def _ _
_ = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) := by {
rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]
}
_ = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c := by ac_rfl
