dist — Mathlib

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)

Похожие утверждения