symmDiff_eq_sup

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#Disjoint.symmDiff_eq_sup

English

If a and b are disjoint, then a Δ b = a ⊔ b.

Русский

Если a и b дизъjointны, то a Δ b = a ⊔ b.

LaTeX

$$$$ Disjoint(a,b) \\Rightarrow a \\Delta b = a \\lor b $$$$

Lean4

theorem symmDiff_eq_sup {a b : α} (h : Disjoint a b) : a ∆ b = a ⊔ b := by
  rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]

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

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

Разделы

Аффилиация

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