comap_apply — Mathlib

English

If f is injective and maps measurable sets s to measurable f''s, then for any μ on β and any measurable s, the equality comap f μ s = μ (f''s) holds.

Русский

Пусть f инъективна и отображает измеримые множества s в измеримые f''s; тогда для любой меры μ на β и любого измеримого s выполняется равенство comap f μ s = μ (f''s).

LaTeX

$$$\\text{comap } f\\, \\mu\\, s = \\mu (f''s)$$$

Lean4

theorem comap_apply (f : α → β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β)
    (hs : MeasurableSet s) : comap f μ s = μ (f '' s) :=
  comap_apply₀ f μ hfi (fun s hs => (hf s hs).nullMeasurableSet) hs.nullMeasurableSet

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