English
The elements of the closure generated by s are exactly those obtained by evaluating terms with variables in s in M; x ∈ closure_L(s) iff there exists a term t with free variables in s such that t.realize((↑): s → M) = x.
Русский
Элементы замыкания, порожденного s, ровно те, которые достигаются путём вычисления термов над переменными из s в M; x ∈ closure_L(s) тогда и только тогда, существует терм t с свободными переменными из s, для которого t.realize((↑): s → M) = x.
LaTeX
$$$$ x \in \operatorname{closure}_L(s) \iff \exists t \in L\mathrm{Term}(s), \ t.realize((\uparrow) : s \to M) = x. $$$$
Lean4
theorem coe_closure_eq_range_term_realize : (closure L s : Set M) = range (@Term.realize L _ _ _ ((↑) : s → M)) :=
by
let S : L.Substructure M :=
⟨range (Term.realize (L := L) ((↑) : s → M)), fun {n} f x hx =>
by
simp only [mem_range] at *
refine ⟨func f fun i => Classical.choose (hx i), ?_⟩
simp only [Term.realize, fun i => Classical.choose_spec (hx i)]⟩
change _ = (S : Set M)
rw [← SetLike.ext'_iff]
refine closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => ?_)
rintro _ ⟨t, rfl⟩
exact t.realize_mem _ fun i => hS' i.2
