biUnion — Mathlib

English

Finite union of constructible sets is constructible.

Русский

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

LaTeX

$$$\text{Finite}(t) \rightarrow (\forall i \in t, \text{IsConstructible}(f(i))) \rightarrow \text{IsConstructible}(\bigcup_{i\in t} f(i))$$$

Lean4

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

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