re — Mathlib · SciLib

English

If f and g are AEStronglyMeasurable, then the function t ↦ ⟪f(t), g(t)⟫ is AEStronglyMeasurable.

Русский

Пусть f и g — AEStronglyMeasurable, тогда t ↦ ⟪f(t), g(t)⟫ имеет AES-сильную измеряемость.

LaTeX

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

Lean4

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

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