oneLePart — Mathlib

English

If f is measurable, then the map x ↦ oneLePart(f(x)) is measurable.

Русский

Пусть f измерима; тогда x ↦ oneLePart(f(x)) также измерима.

LaTeX

$$$\operatorname{Measurable}(f) \Rightarrow \operatorname{Measurable}\bigl(x \mapsto \mathrm{oneLePart}(f(x))\bigr)$$$

Lean4

@[to_additive (attr := measurability)]
protected theorem oneLePart [MeasurableSup α] (hf : Measurable f) : Measurable fun x ↦ oneLePart (f x) :=
  measurable_oneLePart.comp hf

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