comp_stronglyMeasurable — Mathlib

English

If g is continuous and f is strongly measurable, then the composition g∘f is strongly measurable.

Русский

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

LaTeX

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

Lean4

theorem _root_.Continuous.comp_stronglyMeasurable {_ : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ]
    {g : β → γ} {f : α → β} (hg : Continuous g) (hf : StronglyMeasurable f) : StronglyMeasurable fun x => g (f x) :=
  ⟨fun n => SimpleFunc.map g (hf.approx n), fun x => (hg.tendsto _).comp (hf.tendsto_approx x)⟩

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