subset_disjSum

Mathlib.Data.Finset.Sum

URI: https://scilib.ai/kg/mathlib#Finset.subset_disjSum

English

A version of subset relation: u ⊆ s ⊎ t is equivalent to u^{toLeft} ⊆ s and u^{toRight} ⊆ t.

Русский

Версия отношения включения: u ⊆ s ⊎ t эквивалентно u^{toLeft} ⊆ s и u^{toRight} ⊆ t.

LaTeX

$$u \subseteq s \uplus t \iff u^{\mathrm{toLeft}} \subseteq s \land u^{\mathrm{toRight}} \subseteq t$$

Lean4

theorem subset_disjSum : u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t := by simp [subset_iff]

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

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

Разделы

Аффилиация

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