symmDiff_le

Mathlib.Order.SymmDiff

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

English

If a ≤ b ⊔ c and b ≤ a ⊔ c, then a Δ b ≤ c.

Русский

Если a ≤ b ⊔ c и b ≤ a ⊔ c, то a Δ b ≤ c.

LaTeX

$$$$ (a \\le b \\lor c) \\land (b \\le a \\lor c) \\Rightarrow a \\Delta b \\le c $$$$

Lean4

theorem symmDiff_le {a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ∆ b ≤ c :=
  sup_le (sdiff_le_iff.2 ha) <| sdiff_le_iff.2 hb

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

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

Разделы

Аффилиация

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