symmDiff_triangle

Mathlib.Order.SymmDiff

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

← MathLib Explorer

English

For all a,b,c, a Δ c ≤ (a Δ b) ∪ (b Δ c).

Русский

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

LaTeX

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

Lean4

theorem symmDiff_triangle : a ∆ c ≤ a ∆ b ⊔ b ∆ c :=
  by
  refine (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_
  rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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