symmDiff_self

Mathlib.Order.SymmDiff

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

English

Symmetric difference of an element with itself is bottom: a Δ a = ⊥.

Русский

Симметрическая разность элемента самого с собой равна нулю: a Δ a = ⊥.

LaTeX

$$$\\\\forall a \\\\in α, \\\\ symmDiff a a = ⊥$$$

Lean4

@[simp]
theorem symmDiff_self : a ∆ a = ⊥ := by rw [symmDiff, sup_idem, sdiff_self]

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

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

Разделы

Аффилиация

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