biUnion — Mathlib

English

If t is finite and each f(i) with i ∈ t is retrocompact, then the double union ⋃ i ∈ t f(i) is retrocompact.

Русский

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

LaTeX

$$$\text{Finite}(t) \;\Rightarrow\; (\forall i \in t, \text{IsRetrocompact}(f(i))) \Rightarrow \text{IsRetrocompact}(\\bigcup_{i \in t} f(i))$$$

Lean4

theorem biUnion {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) (hf : ∀ i ∈ t, IsRetrocompact (f i)) :
    IsRetrocompact (⋃ i ∈ t, f i) :=
  supClosed_isRetrocompact.biSup_mem ht .empty hf

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