English
Pulling back a measure along a measurable embedding preserves inner regularity: if μ has inner regularity with respect to families p, q, then μ pulled back by f has inner regularity with respect to pa, qa under natural compatibility conditions (images of qa-sets remain qb-sets and preimages of pb-sets lie in pa).
Русский
При обратном образе меры по измеримому вложению сохраняется внутренняя регулярность: если μ имеет внутреннюю регулярность по парам p, q, то обратно-образная мера μ через f обладает внутренней регулярностью по pa, qa при естественных совместимости условий (образы qa-множеств принадлежат qb, прообраз pb-множеств лежит в pa).
LaTeX
$$$\forall \alpha \beta [MeasurableSpace\ \alpha] [MeasurableSpace\ \beta], \forall (H: InnerRegularWRT\ μ\ pb\ qb), \forall f: \alpha \to \beta\, (hf: MeasurableEmbedding\ f), \forall (hAB: \forall U, qa\ U \to qb\ (f``U)), \forall (hAB': \forall K \subseteq range\ f, pb\ K \to pa\ (f^{-1}'K)), \ (μ.comap f).InnerRegularWRT pa qa.$$$
Lean4
protected theorem comap {α β} [MeasurableSpace α] {mβ : MeasurableSpace β} {μ : Measure β} {pa qa : Set α → Prop}
{pb qb : Set β → Prop} (H : InnerRegularWRT μ pb qb) {f : α → β} (hf : MeasurableEmbedding f)
(hAB : ∀ U, qa U → qb (f '' U)) (hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)) : (μ.comap f).InnerRegularWRT pa qa :=
by
intro U hU r hr
rw [hf.comap_apply] at hr
obtain ⟨K, hKU, hK, hμU⟩ := H (hAB U hU) r hr
have hKrange := hKU.trans (image_subset_range _ _)
refine ⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩
· rw [← hf.injective.preimage_image U]; exact preimage_mono hKU
· rwa [hf.comap_apply, image_preimage_eq_iff.mpr hKrange]
