English
A is definable from s iff there exists a finite subcollection A0 ⊆ A that definably realizes s, and conversely.
Русский
Определяемость A по s эквивалентна существованию конечной подмножности A0, подмножество A и definable-s, и обратно.
LaTeX
$$$A.Definable L s \iff \exists A0 : Finset M, (A0 : Set M) \subseteq A \wedge (A0 : Set M).Definable L s.$$$
Lean4
theorem definable_iff_finitely_definable :
A.Definable L s ↔ ∃ (A0 : Finset M), (A0 : Set M) ⊆ A ∧ (A0 : Set M).Definable L s := by
classical
constructor
· simp only [definable_iff_exists_formula_sum]
rintro ⟨φ, rfl⟩
let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
refine
⟨A0, by simp [A0],
(φ.restrictFreeVar <| fun x =>
Sum.casesOn x.1 (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2),
?_⟩
ext
simp only [Formula.Realize, mem_setOf_eq, Finset.coe_sort_coe]
exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)
· rintro ⟨A0, hA0, hd⟩
exact Definable.mono hd hA0
