sUnion_subset

Mathlib.Data.Set.Lattice

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

English

If every member t' ∈ S is contained in t, then the union of S is contained in t.

Русский

Если каждый элемент t' ∈ S удовлетворяет t' ⊆ t, тогда ⋃S ⊆ t.

LaTeX

$$$ (\forall t' \in S, t' \subseteq t) \Rightarrow \bigcup S \subseteq t $$$

Lean4

theorem sUnion_subset {S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t' ⊆ t) : ⋃₀ S ⊆ t :=
  sSup_le h

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

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

Разделы

Аффилиация

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