sumMap — Mathlib

English

If f: α → β and g: γ → δ are measurable, then Sum.map f g : α ⊕ γ → β ⊕ δ is measurable.

Русский

Если f: α → β и g: γ → δ измеримы, то Sum.map f g : α ⊕ γ → β ⊕ δ измеримо.

LaTeX

$$$\mathrm{Measurable}(f) \land \mathrm{Measurable}(g) \Rightarrow \mathrm{Measurable}(\mathrm{Sum.map}(f,g))$$$

Lean4

theorem sumMap {_ : MeasurableSpace γ} {_ : MeasurableSpace δ} {f : α → β} {g : γ → δ} (hf : Measurable f)
    (hg : Measurable g) : Measurable (Sum.map f g) :=
  (measurable_inl.comp hf).sumElim (measurable_inr.comp hg)

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