iUnion — Mathlib

English

For a finite index set, the union of locally constructible sets is locally constructible.

Русский

Для конечного множества индексов объединение локально конструируемых множеств локально конструируемо.

LaTeX

$$$IsLocallyConstructible(\\bigcup_{i\\in F} f(i))$ for finite F.$$

Lean4

theorem iUnion [Finite ι] {f : ι → Set X} (hf : ∀ i, IsLocallyConstructible (f i)) :
    IsLocallyConstructible (⋃ i, f i) :=
  SupClosed.iSup_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.union) .empty hf

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