English
The realization of a term t in the ultraproduct equals the quotient of the pointwise realizations t in each M(a). That is, the interpretation of a term commutes with taking the ultraproduct.
Русский
Реализация терма t в ультропроизведении равна классу по координатам реализации t в каждом M(a). Это говорит о том, что интерпретация терма коммутирует с построением ультропроизведения.
LaTeX
$$$t^{ultra}((x_i)) = [a \mapsto t^{M(a)}(x_i(a))]$$$
Lean4
theorem term_realize_cast {β : Type*} (x : β → ∀ a, M a) (t : L.Term β) :
(t.realize fun i => (x i : (u : Filter α).Product M)) =
(fun a => t.realize fun i => x i a : (u : Filter α).Product M) :=
by
convert
@Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M) (Ultraproduct.setoidPrestructure M u) _ t x using 2
ext a
induction t with
| var => rfl
| func _ _ t_ih => simp only [Term.realize, t_ih]; rfl
