le_comap_apply — Mathlib

English

Let f: α → β be injective and assume that for every measurable set s, the image f''s is null-measurable with respect to μ. Then for every subset s ⊆ α, μ(f''s) ≤ (comap f μ)(s).

Русский

Пусть f: α → β взаимно однозначна и пусть для любого измеримого множества s выполняется, что f''s является нулем-мезурируемым относительно μ. Тогда для любого подмножества s ⊆ α верно |μ(f''s)| ≤ (comap f μ)(s).

LaTeX

$$$\\forall s \\subseteq \\alpha,\\ \\mu(f''s) \\le (\\mathrm{comap}\\ f\\, \\mu)(s)$$$

Lean4

theorem le_comap_apply (f : α → β) (μ : Measure β) (hfi : Injective f)
    (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) (s : Set α) : μ (f '' s) ≤ comap f μ s :=
  by
  rw [comap, dif_pos (And.intro hfi hf)]
  exact le_toMeasure_apply _ _ _

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