iUnion_subset

Mathlib.Data.Set.Lattice

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

English

If every s_i is contained in t, then the union over i of s_i is contained in t.

Русский

Если каждый s_i ⊆ t, то объединение ⋃ i s_i ⊆ t.

LaTeX

$$$\\forall i, s(i) \\subseteq t \\Rightarrow \\bigcup_i s(i) \\subseteq t$$$

Lean4

theorem iUnion_subset {s : ι → Set α} {t : Set α} (h : ∀ i, s i ⊆ t) : ⋃ i, s i ⊆ t :=
  iSup_le h

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

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

Разделы

Аффилиация

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