symmDiff_eq_bot

Mathlib.Order.SymmDiff

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

English

For all a,b in α, a Δ b = ⊥ if and only if a = b.

Русский

Для любых a,b ∈ α верно: a Δ b = ⊥ тогда и только тогда, когда a = b.

LaTeX

$$$$ a \\Delta b = \\bot \\iff a = b $$$$

Lean4

@[simp]
theorem symmDiff_eq_bot {a b : α} : a ∆ b = ⊥ ↔ a = b := by
  simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]

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

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

Разделы

Аффилиация

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