measurable_fun_sum — Mathlib

English

If f ∘ Sum.inl and f ∘ Sum.inr are measurable, then f is measurable on the sum space.

Русский

Если f ∘ Sum.inl и f ∘ Sum.inr измеримы, тогда f измерим на суммарном пространстве.

LaTeX

$$$\\mathrm{Measurable}(f \\circ \\mathrm{Sum.inl}) \\land \\mathrm{Measurable}(f \\circ \\mathrm{Sum.inr}) \\Rightarrow \\mathrm{Measurable}(f)$$$

Lean4

theorem measurable_fun_sum {_ : MeasurableSpace γ} {f : α ⊕ β → γ} (hl : Measurable (f ∘ Sum.inl))
    (hr : Measurable (f ∘ Sum.inr)) : Measurable f :=
  Measurable.of_comap_le <|
    le_inf (MeasurableSpace.comap_le_iff_le_map.2 <| hl) (MeasurableSpace.comap_le_iff_le_map.2 <| hr)

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