fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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