English
Let s be a finite set of indices and for each i in s let f(i) be a locally constructible set. Then the union over i in s of f(i) is locally constructible.
Русский
Пусть s — конечное множество индексов, и для каждого i в s множество f(i) локально конструируемо. Тогда объединение ⋃_{i∈s} f(i) локально конструируемо.
LaTeX
$$$\\#s<\\infty \\ \\wedge\\ \\forall i\\in s\\, \\operatorname{IsLocallyConstructible}(f(i)) \\;\\Rightarrow\\; \\operatorname{IsLocallyConstructible}\\left(\\bigcup_{i\\in s} f(i)\\right).$$$
Lean4
theorem biUnion {ι : Type*} {f : ι → Set X} {s : Set ι} (hs : s.Finite) (hf : ∀ i ∈ s, IsLocallyConstructible (f i)) :
IsLocallyConstructible (⋃ i ∈ s, f i) :=
SupClosed.biSup_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.union) hs .empty hf
