subset_symmDiff_union_symmDiff_right

Mathlib.Data.Set.SymmDiff

URI: https://scilib.ai/kg/mathlib#Set.subset_symmDiff_union_symmDiff_right

English

If t and u are disjoint, then any s is contained in s Δ t ∪ s Δ u.

Русский

Если t и u несоседны, то любой s содержится в s Δ t ∪ s Δ u.

LaTeX

$$$h : \\text{Disjoint } t u \\Rightarrow s \\subseteq s \\Delta t \\cup s \\Delta u$$$

Lean4

theorem subset_symmDiff_union_symmDiff_right (h : Disjoint t u) : s ⊆ s ∆ t ∪ s ∆ u :=
  h.le_symmDiff_sup_symmDiff_right

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

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

Разделы

Аффилиация

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