union_subset_union

Mathlib.Data.Finset.Lattice.Basic

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

English

If S ⊆ U and T ⊆ V, then S ∪ T ⊆ U ∪ V.

Русский

Если S ⊆ U и T ⊆ V, то S ∪ T ⊆ U ∪ V.

LaTeX

$$$ s \subseteq u \Rightarrow t \subseteq v \Rightarrow (s \cup t) \subseteq (u \cup v) $$$

Lean4

@[gcongr]
theorem union_subset_union (hsu : s ⊆ u) (htv : t ⊆ v) : s ∪ t ⊆ u ∪ v :=
  sup_le_sup (le_iff_subset.2 hsu) htv

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

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

Разделы

Аффилиация

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