α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
μ : Measure α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : BorelSpace β
inst✝ : Regular μ
f : α ≃ₜ β
this : OuterRegular (map (↑f) μ)
⊢ Regular (map (↑f) μ)
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
μ : Measure α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : BorelSpace β
inst✝ : Regular μ
f : α ≃ₜ β
⊢ Regular (map (↑f) μ)
haveI := OuterRegular.map f μ
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
μ : Measure α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : BorelSpace β
inst✝ : Regular μ
f : α ≃ₜ β
this✝ : OuterRegular (map (↑f) μ)
this : IsFiniteMeasureOnCompacts (map (↑f) μ)
⊢ Regular (map (↑f) μ)
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
μ : Measure α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : BorelSpace β
inst✝ : Regular μ
f : α ≃ₜ β
this : OuterRegular (map (↑f) μ)
⊢ Regular (map (↑f) μ)
haveI := IsFiniteMeasureOnCompacts.map μ f
no goals
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
μ : Measure α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : BorelSpace β
inst✝ : Regular μ
f : α ≃ₜ β
this✝ : OuterRegular (map (↑f) μ)
this : IsFiniteMeasureOnCompacts (map (↑f) μ)
⊢ Regular (map (↑f) μ)
exact
  ⟨Regular.innerRegular.map f.toEquiv f.measurable.aemeasurable
      (fun U hU => hU.preimage f.continuous) (fun K hK => hK.image f.continuous)
      (fun K hK => hK.measurableSet) fun U hU => hU.measurableSet⟩