English
The action of a function symbol on the ultraproduct obtained by quotienting is compatible with the quotient of the action on the coordinates; i.e., applying funMap in the ultraproduct to (f) and (x_i) is the same as taking the quotient of the coordinatewise applications.
Русский
Действие символьной функции на ультропроизведении, полученном путем факторизации, совместимо с действием на координатах: применить funMap в ультропроизведении к (f) и (x_i) эквивалентно взятию класс по координатам.
LaTeX
$$$\mathrm{Quotient.mk'}(\text{(x_i) }) = \mathrm{Quotient.mk'}(\lambda a\, (\mathrm{inst}(a).\mathrm{funMap}_L(f))(x_i(a)))$$$
Lean4
theorem funMap_cast {n : ℕ} (f : L.Functions n) (x : Fin n → ∀ a, M a) :
(funMap f fun i => (x i : (u : Filter α).Product M)) =
(fun a => funMap f fun i => x i a : (u : Filter α).Product M) :=
by apply funMap_quotient_mk'
