symmDiff_eq_left

Mathlib.Order.SymmDiff

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

← MathLib Explorer

English

a Δ b = a ⇔ b = ⊥

Русский

a Δ b = a ⇔ b = ⊥

LaTeX

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

Lean4

@[simp]
theorem symmDiff_eq_left : a ∆ b = a ↔ b = ⊥ :=
  calc
    a ∆ b = a ↔ a ∆ b = a ∆ ⊥ := by rw [symmDiff_bot]
    _ ↔ b = ⊥ := by rw [symmDiff_right_inj]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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