le_symmDiff_sup_symmDiff_right

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#Disjoint.le_symmDiff_sup_symmDiff_right

← MathLib Explorer

English

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

Русский

Если b и c несовместны, то a ≤ a Δ b ⊔ a Δ c.

LaTeX

$$$ (h : Disjoint b c) ": a \\leq a \\triangle b \\sqcup a \\triangle c $$$

Lean4

theorem le_symmDiff_sup_symmDiff_right (h : Disjoint b c) : a ≤ a ∆ b ⊔ a ∆ c :=
  by
  simp_rw [symmDiff_comm a]
  exact h.le_symmDiff_sup_symmDiff_left

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

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

Разделы

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

Аффилиация

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