definable_finset_sup — Mathlib

English

Definability is closed under finite supremums; the union over a finite index set of definable families is definable.

Русский

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

LaTeX

$$$(\forall i, A.Definable L (f i)) \rightarrow \forall s : Finset ι, A.Definable L (s.sup f).$$$

Lean4

theorem definable_finset_sup {ι : Type*} {f : ι → Set (α → M)} (hf : ∀ i, A.Definable L (f i)) (s : Finset ι) :
    A.Definable L (s.sup f) := by
  classical
  refine Finset.induction definable_empty (fun i s _ h => ?_) s
  rw [Finset.sup_insert]
  exact (hf i).union h

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