comap_preimage — Mathlib

English

For an injective f and measurable f, the comap of a μ-measure on β with the preimage of s equals μ on s ∩ range(f).

Русский

При инъективности f и измеримости f предобраз множества s удовлетворяет: comap f μ (s) = μ (s ∩ range f).

LaTeX

$$$\\mu.comap f (f^{-1}'s) = \\mu (s \\cap \\mathrm{range} f)$$$

Lean4

theorem comap_preimage (f : α → β) (μ : Measure β) (hf : Injective f) (hf' : Measurable f)
    (h : ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ) {s : Set β} (hs : MeasurableSet s) :
    μ.comap f (f ⁻¹' s) = μ (s ∩ range f) := by
  rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]

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