le_symmDiff_sup_left

Mathlib.Order.SymmDiff

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

English

For all a,b, b ≤ (a Δ b) ⊔ a.

Русский

Для любых a,b: b ≤ (a Δ b) ⊔ a.

LaTeX

$$$$ b \\le (a \\Delta b) \\lor a $$$$

Lean4

theorem le_symmDiff_sup_left (a b : α) : b ≤ (a ∆ b) ⊔ a :=
  symmDiff_comm a b ▸ le_symmDiff_sup_right ..

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

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

Разделы

Аффилиация

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