map' — Mathlib

English

If μ is inner regular with p, q and f is a measurable equivalence, then InnerRegularWRT for map f μ holds with pb, qb under hAB, hAB'.

Русский

Если μ внутренняя регулярность по p, q и f измеримое эквивалентное отображение, то свойство внутренней регулярности сохраняется для map f μ.

LaTeX

$$∞$$

Lean4

theorem map' {α β} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {pa qa : Set α → Prop}
    (H : InnerRegularWRT μ pa qa) (f : α ≃ᵐ β) {pb qb : Set β → Prop} (hAB : ∀ U, qb U → qa (f ⁻¹' U))
    (hAB' : ∀ K, pa K → pb (f '' K)) : InnerRegularWRT (map f μ) pb qb :=
  by
  intro U hU r hr
  rw [f.map_apply U] at hr
  rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
  refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
  rwa [f.map_apply, f.preimage_image]

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