definable_finset_inf — Mathlib

English

Definability is closed under finite infimums; the intersection 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.inf f).$$$

Lean4

theorem definable_finset_inf {ι : Type*} {f : ι → Set (α → M)} (hf : ∀ i, A.Definable L (f i)) (s : Finset ι) :
    A.Definable L (s.inf f) := by
  classical
  refine Finset.induction definable_univ (fun i s _ h => ?_) s
  rw [Finset.inf_insert]
  exact (hf i).inter h

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