symmDiff_right_comm

Mathlib.Order.SymmDiff

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

English

A higher-order identity expressing a commutation of nested symmetric differences: symmDiff_symmDiff_symmDiff_comm.

Русский

Высшее свойство коммутативности вложенных симмDiff.

LaTeX

$$∀ a b c d, symmDiff_symmDiff_symmDiff_comm a b c d$$

Lean4

theorem symmDiff_right_comm : a ∆ b ∆ c = a ∆ c ∆ b := by simp_rw [symmDiff_assoc, symmDiff_comm]

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

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

Разделы

Аффилиация

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