English
The pairing operation combines two almost-everywhere equal functions into a single function with values in the product β × γ, carrying the appropriate measurability data.
Русский
Оператор сцепления объединяет две функции, равные almost everywhere, в одну функцию с значения́ми в произведении β × γ, сохраняя соответствующую измеримость.
LaTeX
$$$\text{pair}(f,g) : α →ₘ[μ] β × γ$ is defined by $x \mapsto (f(x), g(x))$ with the natural product measurability data.$$
Lean4
/-- The class of `x ↦ (f x, g x)`. -/
def pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : α →ₘ[μ] β × γ :=
Quotient.liftOn₂' f g (fun f g => mk (fun x => (f.1 x, g.1 x)) (f.2.prodMk g.2)) fun _f _g _f' _g' Hf Hg =>
mk_eq_mk.2 <| Hf.prodMk Hg
