English
A Definable set A from parameters s in language L is equivalent to the existence of a formula φ in L with free variables in A ⊕ α such that s describes the realizations of φ with respect to Sum.elim.
Русский
Определяемость множества A из параметров s в языке L эквивалентна существованию формулы φ в L с свободными переменными в A ⊕ α, такая что s описывает реализции φ через Sum.elim.
LaTeX
$$$A\Definable L s \iff \exists \phi : L.Formula (A \oplus \alpha),\ s = \{v \mid \phi.Realize (Sum.elim (\uparrow) v)\}.$$$
Lean4
theorem definable_iff_exists_formula_sum :
A.Definable L s ↔ ∃ φ : L.Formula (A ⊕ α), s = {v | φ.Realize (Sum.elim (↑) v)} :=
by
rw [Definable, Equiv.exists_congr_left (BoundedFormula.constantsVarsEquiv)]
refine exists_congr (fun φ => iff_iff_eq.2 (congr_arg (s = ·) ?_))
ext
simp only [BoundedFormula.constantsVarsEquiv, constantsOn, BoundedFormula.mapTermRelEquiv_symm_apply, mem_setOf_eq,
Formula.Realize]
refine BoundedFormula.realize_mapTermRel_id ?_ (fun _ _ _ => rfl)
intros
simp only [Term.constantsVarsEquivLeft_symm_apply, Term.realize_varsToConstants, coe_con, Term.realize_relabel]
congr 1 with a
rcases a with (_ | _) | _ <;> rfl
