definable_biUnion_finset — Mathlib

English

Definability of intersections over a Finset: finite intersections of definable families are definable.

Русский

Определяемость пересечений по Finset: конечные пересечения определимы.

LaTeX

$$$A.Definable L (⋂ i ∈ s, f i).$$$

Lean4

theorem definable_biUnion_finset {ι : Type*} {f : ι → Set (α → M)} (hf : ∀ i, A.Definable L (f i)) (s : Finset ι) :
    A.Definable L (⋃ i ∈ s, f i) := by
  rw [← Finset.sup_set_eq_biUnion]
  exact definable_finset_sup hf s

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