sUnion_subset_sUnion

Mathlib.Data.Set.Lattice

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

English

If S ⊆ T, then ⋃S ⊆ ⋃T.

Русский

Если S ⊆ T, тогда ⋃S ⊆ ⋃T.

LaTeX

$$$ S \subseteq T \rightarrow \bigcup S \subseteq \bigcup T $$$

Lean4

@[gcongr]
theorem sUnion_subset_sUnion {S T : Set (Set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T :=
  sUnion_subset fun _ hs => subset_sUnion_of_mem (h hs)

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

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

Разделы

Аффилиация

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