English
For a fixed m, a definable set s under Sum α (Fin m) → M can be mapped via Sum.inl to another definable set.
Русский
Для фиксированного m множество s заметно определимо под отображением Sum.inl.
LaTeX
$$$\forall m, A.Definable L s \rightarrow A.Definable L ((\text{fun } g : Sum \alpha (Fin m) \to M => g \circ Sum.inl) '' s).$$$
Lean4
/-- This lemma is only intended as a helper for `Definable.image_comp`. -/
theorem image_comp_sumInl_fin (m : ℕ) {s : Set (Sum α (Fin m) → M)} (h : A.Definable L s) :
A.Definable L ((fun g : Sum α (Fin m) → M => g ∘ Sum.inl) '' s) :=
by
obtain ⟨φ, rfl⟩ := h
refine ⟨(BoundedFormula.relabel id φ).exs, ?_⟩
ext x
simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs, BoundedFormula.realize_relabel, Function.comp_id,
Fin.castAdd_zero, Fin.cast_refl]
constructor
· rintro ⟨y, hy, rfl⟩
exact ⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩
· rintro ⟨y, hy⟩
exact ⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩
