iUnion — Mathlib

English

If ι is finite and each f(i) is retrocompact, then the union ⋃ i f(i) is retrocompact.

Русский

Если индексное множество ι конечное и каждый f(i) ретрокомпактно, то их объединение ретрокомпактно.

LaTeX

$$$[Finite\ ι]\; \forall i, IsRetrocompact(f(i)) \Rightarrow IsRetrocompact(\\bigcup_i f(i))$$$

Lean4

theorem iUnion [Finite ι] {f : ι → Set X} (hf : ∀ i, IsRetrocompact (f i)) : IsRetrocompact (⋃ i, f i) :=
  supClosed_isRetrocompact.iSup_mem .empty hf

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