comp_measurable — Mathlib

English

If f is strongly measurable and g is measurable, then f∘g is strongly measurable.

Русский

Если f сильно измерима, а g измерима, то композиция f∘g сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \land \text{Measurable}(g) \Rightarrow \text{StronglyMeasurable}(f \circ g)$$$

Lean4

@[fun_prop]
theorem comp_measurable [TopologicalSpace β] {_ : MeasurableSpace α} {_ : MeasurableSpace γ} {f : α → β} {g : γ → α}
    (hf : StronglyMeasurable f) (hg : Measurable g) : StronglyMeasurable (f ∘ g) :=
  ⟨fun n => SimpleFunc.comp (hf.approx n) g hg, fun x => hf.tendsto_approx (g x)⟩

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