comap_apply₀ — Mathlib

English

Generalized statement linking comap with image under f for measurable s.

Русский

Обобщённое утверждение о связи comap и образа через отображение.

LaTeX

$$$\operatorname{comap}(f) μ(s) = μ(f''s)$$$

Lean4

theorem comap_apply₀ (f : α → β) (μ : Measure β) (hfi : Injective f)
    (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) (hs : NullMeasurableSet s (comap f μ)) :
    comap f μ s = μ (f '' s) := by
  rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢
  rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]

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