sup — Mathlib

English

The product of a finite list of strongly measurable functions is strongly measurable provided each is strongly measurable.

Русский

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

LaTeX

$$$\forall l:\text{List}(\alpha \to M), \ (\forall f \in l, \text{StronglyMeasurable } f) \Rightarrow \text{StronglyMeasurable } (\lambda a, \prod_{f \in l} f(a))$$$

Lean4

@[fun_prop, aesop safe 20 (rule_sets := [Measurable])]
protected theorem sup [Max β] [ContinuousSup β] (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable (f ⊔ g) :=
  ⟨fun n => hf.approx n ⊔ hg.approx n, fun x => (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩

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