English
Definability is preserved under finite embeddings with a bound on the codomain; image under an embedding of a definable set remains definable.
Русский
Определяемость сохраняется под конечной вложенной отображением; образ definable остаётся definable.
LaTeX
$$$A.Definable L s \rightarrow \forall (f : \alpha \hookrightarrow \beta) [Finite \beta], A.Definable L (Set.image (fun g => g \circ (Function.instFunLikeEmbedding.coe f)) s).$$$
Lean4
/-- Shows that definability is closed under finite projections. -/
theorem image_comp_embedding {s : Set (β → M)} (h : A.Definable L s) (f : α ↪ β) [Finite β] :
A.Definable L ((fun g : β → M => g ∘ f) '' s) := by
classical
cases nonempty_fintype β
refine
(congr rfl (ext fun x => ?_)).mp
(((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
(Equiv.sumCongr (Equiv.ofInjective f f.injective)
(Fintype.equivFin (↥(range f)ᶜ)).symm)).image_comp_sumInl_fin
_)
simp only [mem_image, exists_exists_and_eq_and]
refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
simp
