comapₗ_apply — Mathlib

English

If f is injective and maps measurableSets to measurable, then comap f μ s = μ(f''s) for measurable s.

Русский

Если f инъективно отображает измеримые множества в измеримые, то comap f μ s = μ(f '' s) для измеримого s.

LaTeX

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

Lean4

theorem comapₗ_apply {_ : MeasurableSpace α} {_ : MeasurableSpace β} (f : α → β) (hfi : Injective f)
    (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) (hs : MeasurableSet s) :
    comapₗ f μ s = μ (f '' s) :=
  by
  rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]
  exact ⟨hfi, hf⟩

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