sdiff_symmDiff'

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#sdiff_symmDiff'

English

An alternate form of the sdif/symmdiff relation: c \\ a Δ b = c ∧ a ∧ b ∨ c \\ (a ∨ b).

Русский

Альтернативная форма: c \\ a Δ b = c ∧ a ∧ b ∨ c \\ (a ∨ b).

LaTeX

$$∀ a b c, c \\ a ∆ b = c ∧ a ∧ b ∨ c \\ (a ∨ b)$$

Lean4

theorem sdiff_symmDiff' : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b) := by rw [sdiff_symmDiff, sdiff_sup]

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

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

Разделы

Аффилиация

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