sUnion_subset_iff

Mathlib.Data.Set.Lattice

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

English

The union is contained in t if and only if every member is contained in t.

Русский

Объединение ⊆ t тогда и только тогда, когда каждый элемент множества принадлежит t.

LaTeX

$$$ \bigcup S \subseteq t \iff \forall t' \in S, t' \subseteq t $$$

Lean4

@[simp]
theorem sUnion_subset_iff {s : Set (Set α)} {t : Set α} : ⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t :=
  sSup_le_iff

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

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

Разделы

Аффилиация

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