measurable_comp_iff — Mathlib

English

Let f: α → β and g: β → γ with g a MeasurableEmbedding. Then g ∘ f is measurable if and only if f is measurable.

Русский

Пусть f: α → β и g: β → γ, причём g является измеримым вложением. Тогда композиция g ∘ f измерима тогда и только тогда, когда f измерим.

LaTeX

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

Lean4

theorem measurable_comp_iff (hg : MeasurableEmbedding g) : Measurable (g ∘ f) ↔ Measurable f :=
  by
  refine ⟨fun H => ?_, hg.measurable.comp⟩
  suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
  exact hg.measurable_rangeSplitting.comp H.subtype_mk

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