comp_fst — Mathlib

English

If f is strongly measurable, then the function z ↦ f(z.1) is strongly measurable on α×β.

Русский

Если f сильно измерима, то z ↦ f(z.1) на α×β сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \text{StronglyMeasurable}(z \mapsto f(z.1))$$$

Lean4

protected theorem comp_fst {_ : MeasurableSpace α} [mβ : MeasurableSpace β] [TopologicalSpace γ] {f : α → γ}
    (hf : StronglyMeasurable f) : StronglyMeasurable (fun z : α × β => f z.1) :=
  hf.comp_measurable measurable_fst

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