symmDiff_isAssociative

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#symmDiff_isAssociative

English

Symmetric difference is associative: a Δ b Δ c = a Δ (b Δ c).

Русский

Симметрическая разность ассоциативна: a Δ b Δ c = a Δ (b Δ c).

LaTeX

$$∀ a b c, a ∆ b ∆ c = a ∆ (b ∆ c)$$

Lean4

instance symmDiff_isAssociative : Std.Associative (α := α) (· ∆ ·) :=
  ⟨symmDiff_assoc⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru