iUnion_subset_iUnion_const — Mathlib

English

For any fixed subset s ⊆ α, the union over i of s equals the union over i₂ of s, i.e., the union does not depend on the index set when the family is constant: ⋃ i, s ⊆ ⋃ i₂, s.

Русский

Для неподвижного подмножества s ⊆ α объединение по i равно объединению по i₂: ⋃ i, s ⊆ ⋃ i₂, s.

LaTeX

$$$$ \\bigcup_{i} s \\subseteq \\bigcup_{i' } s. $$$$

Lean4

theorem iUnion_subset_iUnion_const {s : Set α} (h : ι → ι₂) : ⋃ _ : ι, s ⊆ ⋃ _ : ι₂, s :=
  iSup_const_mono (α := Set α) h

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