comapₗ_eq_comap — Mathlib

English

For an injective f with the same measurability condition as above, the linearized comap coincides with the standard comap: comapₗ f μ s = comap f μ s for all measurable s.

Русский

При той же инъективности f и соответствующих ограничениях на измеримость, линейная версия комап совпадает с обычной: comapₗ f μ s = comap f μ s для всех измеримых s.

LaTeX

$$$\\forall s\\, (\\text{MeasurableSet } s),\\ comap\\_l f\\, \\mu\\, s = comap f\\, \\mu\\, s$$$

Lean4

theorem comapₗ_eq_comap (f : α → β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s))
    (μ : Measure β) (hs : MeasurableSet s) : comapₗ f μ s = comap f μ s :=
  (comapₗ_apply f hfi hf μ hs).trans (comap_apply f hfi hf μ hs).symm

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