English
The pair operation on AEEqFun is representation-equivalent to constructing a mk from the pair of the underlying functions.
Русский
Операция пары на AEEqFun эквивалентна конструированию mk из пары базовых функций.
LaTeX
$$$f.pair g = mk(\lambda x, (f(x), g(x)))\ (f.aestronglyMeasurable.prodMk g.aestronglyMeasurable)$$$
Lean4
theorem pair_eq_mk (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
f.pair g = mk (fun x => (f x, g x)) (f.aestronglyMeasurable.prodMk g.aestronglyMeasurable) := by
simp only [← pair_mk_mk, mk_coeFn, f.aestronglyMeasurable, g.aestronglyMeasurable]