α : Type u_1
β : Type ?u.71015
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : Regular μ
x : ℝ≥0∞
hx : x ≠ ⊤
this : OuterRegular (x • μ)
⊢ Regular (x • μ)
α : Type u_1
β : Type ?u.71015
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : Regular μ
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ Regular (x • μ)
haveI := OuterRegular.smul μ hx
α : Type u_1
β : Type ?u.71015
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : Regular μ
x : ℝ≥0∞
hx : x ≠ ⊤
this✝ : OuterRegular (x • μ)
this : IsFiniteMeasureOnCompacts (x • μ)
⊢ Regular (x • μ)
α : Type u_1
β : Type ?u.71015
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : Regular μ
x : ℝ≥0∞
hx : x ≠ ⊤
this : OuterRegular (x • μ)
⊢ Regular (x • μ)
haveI := IsFiniteMeasureOnCompacts.smul μ hx
no goals
α : Type u_1
β : Type ?u.71015
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : Regular μ
x : ℝ≥0∞
hx : x ≠ ⊤
this✝ : OuterRegular (x • μ)
this : IsFiniteMeasureOnCompacts (x • μ)
⊢ Regular (x • μ)
exact ⟨Regular.innerRegular.smul x⟩