iUnion₂_subset_iUnion — Mathlib

English

For κ : ι → Sort and s : ι → Set α, the double-index union is contained in the single-index union: ⋃_i (⋃_({_: κ i}) s_i) ⊆ ⋃_i s_i.

Русский

Для κ : ι → Sort и семейства s_i ⊆ α, двойной индекс объединения содержится в одинарном: ⋃_i ⋃_{j} s_i ⊆ ⋃_i s_i.

LaTeX

$$$\bigcup_{i} \bigcup_{j} s_i \subseteq \bigcup_{i} s_i$$$

Lean4

theorem iUnion₂_subset_iUnion (κ : ι → Sort*) (s : ι → Set α) : ⋃ (i) (_ : κ i), s i ⊆ ⋃ i, s i :=
  iUnion_mono fun _ => iUnion_subset fun _ => Subset.rfl

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