comp' — Mathlib

English

Under MeasurableEmbedding, the composition g ∘ f is measurable.

Русский

При условии измеримости вложений композиция g ∘ f измерима.

LaTeX

$$$\\text{MeasurableEmbedding}(g) \\to \\text{MeasurableEmbedding}(f) \\to \\text{Measurable}(g \\circ f).$$$

Lean4

@[fun_prop, aesop safe 50 (rule_sets := [Measurable])]
protected theorem comp' {_ : MeasurableSpace α} {_ : MeasurableSpace β} {_ : MeasurableSpace γ} {g : β → γ} {f : α → β}
    (hg : Measurable g) (hf : Measurable f) : Measurable (fun x => g (f x)) :=
  Measurable.comp hg hf

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