iUnion_subset_iff — Mathlib

English

Let a family of subsets s_i of α and a fixed subset t be given. Then the union ⋃_i s_i is contained in t if and only if every s_i is contained in t.

Русский

Пусть дано семейство подмножеств s_i ⊆ α и фиксированное множество t. Тогда объединение ⋃_i s_i ⊆ t тогда и только тогда, когда каждое s_i ⊆ t.

LaTeX

$$$\bigcup_{i} s_i \subseteq t \iff \forall i,\ s_i \subseteq t$$$

Lean4

@[simp]
theorem iUnion_subset_iff {s : ι → Set α} {t : Set α} : ⋃ i, s i ⊆ t ↔ ∀ i, s i ⊆ t :=
  ⟨fun h _ => Subset.trans (le_iSup s _) h, iUnion_subset⟩

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