prodMk — Mathlib

English

If f and g are strongly measurable, then x ↦ (f x, g x) is strongly measurable.

Русский

Если f и g сильно измеримы, то функция x ↦ (f x, g x) сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \land \text{StronglyMeasurable}(g) \Rightarrow \text{StronglyMeasurable}(x \mapsto (f(x), g(x)))$$$

Lean4

@[fun_prop]
protected theorem prodMk {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : α → γ}
    (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) : StronglyMeasurable fun x => (f x, g x) :=
  by
  refine ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩
  rw [nhds_prod_eq]
  exact Tendsto.prodMk (hf.tendsto_approx x) (hg.tendsto_approx x)

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