comp — Mathlib

English

If g and f are MeasurableEmbeddings, then their composition g ∘ f is a MeasurableEmbedding.

Русский

Если g и f — измеримые вложения, то композиция g ∘ f является измеримым вложением.

LaTeX

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

Lean4

protected theorem comp {_ : MeasurableSpace α} {_ : MeasurableSpace β} {_ : MeasurableSpace γ} {g : β → γ} {f : α → β}
    (hg : Measurable g) (hf : Measurable f) : Measurable (g ∘ f) := fun _ h =>
  hf
    (hg h)
      -- This is needed due to reducibility issues with the `measurability` tactic.

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