case inl
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
hx : 0 ≠ ⊤
⊢ OuterRegular (0 • μ)

case inr
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
⊢ OuterRegular (x • μ)
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ OuterRegular (x • μ)
rcases eq_or_ne x 0 with (rfl | h0)
case inl
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
hx : 0 ≠ ⊤
⊢ OuterRegular 0
case inl
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
hx : 0 ≠ ⊤
⊢ OuterRegular (0 • μ)
rw [zero_smul]
no goals
case inl
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
hx : 0 ≠ ⊤
⊢ OuterRegular 0
exact OuterRegular.zero
case inr
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑(x • μ) A
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(x • μ) U < r
case inr
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
⊢ OuterRegular (x • μ)
refine' ⟨fun A _ r hr => _⟩
case inr
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(x • μ) U < r
case inr
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑(x • μ) A
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(x • μ) U < r
rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr
no goals
case inr
α : Type u_1
β : Type ?u.15149
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ μ : Measure α
inst✝ : OuterRegular μ
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(x • μ) U < r
simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using hr