symmDiff_bot

Mathlib.Order.SymmDiff

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

English

Symmetric difference with bottom leaves the element unchanged: a Δ ⊥ = a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem symmDiff_bot : a ∆ ⊥ = a := by rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]

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

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

Разделы

Аффилиация

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