star — Mathlib

English

Pointwise star on a function preserves strong measurability: if f is strongly measurable, then x ↦ star(f(x)) is strongly measurable.

Русский

Пусть f — сильно измеримая функция; тогда покомпонентно звездочка над значением функции сохраняет сильную измеримость: x ↦ star(f(x)).

LaTeX

$$$\forall f: \alpha \to R, \text{StronglyMeasurable } f \Rightarrow \text{StronglyMeasurable } (x \mapsto \operatorname{star}(f(x)))$$$

Lean4

/-- Pointwise star on functions induced from continuous star preserves strong measurability. -/
@[measurability]
protected theorem star {R : Type*} [MeasurableSpace α] [Star R] [TopologicalSpace R] [ContinuousStar R] (f : α → R)
    (hf : StronglyMeasurable f) : StronglyMeasurable (star f) :=
  ⟨fun n => star (hf.approx n), fun x => (hf.tendsto_approx x).star⟩

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