im — Mathlib · SciLib

English

For AEStronglyMeasurable f and g, the map x ↦ ⟪f(x), g(x)⟫ is AEStronglyMeasurable.

Русский

Для AEStronglyMeasurable f и g отображение x ↦ ⟪f(x), g(x)⟫ имеет AES-сильную измеряемость.

LaTeX

$$$\text{AEStronglyMeasurable}(f) \Rightarrow \text{AEStronglyMeasurable}(x \mapsto \langle f(x), g(x) \rangle)$$$

Lean4

@[fun_prop]
protected theorem im {f : α → 𝕜} (hf : AEStronglyMeasurable[m] f μ) :
    AEStronglyMeasurable[m] (fun x => RCLike.im (f x)) μ :=
  RCLike.continuous_im.comp_aestronglyMeasurable hf

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