sUnion — Mathlib

English

If S is a finite set of sets and each s ∈ S is retrocompact, then the union ⋃S is retrocompact.

Русский

Если S — конечное множество множеств, и каждое s ∈ S ретрокомпактно, то ⋃S ретрокомпактно.

LaTeX

$$$\text{Finite}(S) \;\Rightarrow\; (\forall s \in S, \text{IsRetrocompact}(s)) \Rightarrow \text{IsRetrocompact}(\bigcup S)$$$

Lean4

theorem sUnion {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsRetrocompact s) : IsRetrocompact (⋃₀ S) :=
  supClosed_isRetrocompact.sSup_mem hS .empty hS'

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