English
If f and g are AEStronglyMeasurable with respect to μ, then the function x ↦ dist(f x, g x) is AEStronglyMeasurable with respect to μ.
Русский
Если f и g — AEStronglyMeasurable по μ, то функция x ↦ dist(f x, g x) является AEStronglyMeasurable по μ.
LaTeX
$$$AEStronglyMeasurable(f, \mu) \land AEStronglyMeasurable(g, \mu) \Rightarrow AEStronglyMeasurable(\nabla x \mapsto dist(f(x), g(x)), \mu)$$$
Lean4
@[fun_prop, aesop safe 20 apply (rule_sets := [Measurable])]
protected theorem dist {β : Type*} [PseudoMetricSpace β] {f g : α → β} (hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (fun x => dist (f x) (g x)) μ :=
continuous_dist.comp_aestronglyMeasurable (hf.prodMk hg)