comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) : MeasurableEmbedding (g ∘ f) :=
  ⟨hg.injective.comp hf.injective, hg.measurable.comp hf.measurable, fun s hs => by
    rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]⟩

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