symmDiff_symmDiff_cancel_left

Mathlib.Order.SymmDiff

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

English

Alternative articulation: a Δ (a Δ b) = b; equivalently, symmDiff_symmDiff_cancel_left.

Русский

Альтернатива: a Δ (a Δ b) = b; эквивалентно symmDiff_cancel_left.

LaTeX

$$∀ a b, Eq (symmDiff a (symmDiff a b)) b$$

Lean4

@[simp]
theorem symmDiff_symmDiff_cancel_left : a ∆ (a ∆ b) = b := by simp [← symmDiff_assoc]

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

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

Разделы

Аффилиация

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