definable_biInter_finset — Mathlib

English

Definability is closed under finite biunion; the union over a finite set is definable.

Русский

Определяемость сохраняется при конечном биобъединении; объединение над конечным множеством определимо.

LaTeX

$$$A.Definable L (\bigcup i \in s, f i).$$$

Lean4

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

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