dist — Mathlib

English

The limit of a sequence of strongly measurable functions is strongly measurable.

Русский

Предел последовательности сильно измеримых функций является сильно измеримым.

LaTeX

$$$\lim_{i\to}\ f_i = g \text{ with } f_i \text{ strongly measurable } \Rightarrow \mathrm{StronglyMeasurable}(g)$$$

Lean4

@[fun_prop, aesop safe 20 apply (rule_sets := [Measurable])]
protected theorem dist {_ : MeasurableSpace α} {β : Type*} [PseudoMetricSpace β] {f g : α → β}
    (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) : StronglyMeasurable fun x => dist (f x) (g x) :=
  continuous_dist.comp_stronglyMeasurable (hf.prodMk hg)

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