edist — Mathlib

English

An induction principle: constants, piecewise, and limits generate all strongly measurable functions.

Русский

Индуктивный принцип: константы, кусочно-зависимые конструирования и пределы порождают все сильно измеримые функции.

LaTeX

$$$\text{induction}'(P)$ expresses that constants, piecewise constructions, and limits suffice to prove P for all strongly measurable functions.$$

Lean4

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

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