symmDiff_sdiff_right

Mathlib.Order.SymmDiff

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

English

Symmetric difference with the other argument equals their intersection: b \\ a Δ b = a ∧ b.

Русский

Симметрическая разность относительно второго аргумента равна пересечению: b \\ a Δ b = a ∧ b.

LaTeX

$$∀ a b, sdiff b (symmDiff a b) = a ∧ b$$

Lean4

@[simp]
theorem symmDiff_sdiff_right : a ∆ b \ b = a \ b := by rw [symmDiff_comm, symmDiff_sdiff_left]

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

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

Разделы

Аффилиация

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