symmDiff_of_ge

Mathlib.Order.SymmDiff

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

English

If b ≤ a, then a Δ b = a \\ b (the part of a not in b).

Русский

Если b ≤ a, то a Δ b = a \\ b (часть a, не входящая в b).

LaTeX

$$$$ b \\le a \\Rightarrow a \\Delta b = a \\setminus b $$$$

Lean4

theorem symmDiff_of_ge {a b : α} (h : b ≤ a) : a ∆ b = a \ b := by rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]

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

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

Разделы

Аффилиация

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