snd — Mathlib

English

If f: α → β×γ is strongly measurable, then its second projection is strongly measurable.

Русский

Если f: α → β×γ сильно измерима, то её вторая проекция (f x)2 сильносильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \text{StronglyMeasurable}(x \mapsto (f(x)).2)$$$

Lean4

@[fun_prop]
protected theorem snd {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ] {f : α → β × γ}
    (hf : StronglyMeasurable f) : StronglyMeasurable fun x ↦ (f x).2 :=
  continuous_snd.comp_stronglyMeasurable hf

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