English
If μ is inner regular with p, q and f is a measurable equivalence, then map f μ is inner regular with pb, qb under suitable transfer conditions.
Русский
Если μ внутренняя регулярность по p, q и f является измеримым эквивалентом, то map f μ является внутренней регулярностью по pb, qb.
LaTeX
$$∞$$
Lean4
protected theorem map {α β} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {pa qa : Set α → Prop}
(H : InnerRegularWRT μ pa qa) {f : α → β} (hf : AEMeasurable f μ) {pb qb : Set β → Prop}
(hAB : ∀ U, qb U → qa (f ⁻¹' U)) (hAB' : ∀ K, pa K → pb (f '' K)) (hB₂ : ∀ U, qb U → MeasurableSet U) :
InnerRegularWRT (map f μ) pb qb := by
intro U hU r hr
rw [map_apply_of_aemeasurable hf (hB₂ _ hU)] at hr
rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
exact hK.trans_le (le_map_apply_image hf _)
