α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U✝ s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
U : Set X
hU : IsOpen U
r : ℝ≥0∞
hr : r < ↑↑μ U
⊢ ∃ K, K ⊆ U ∧ IsClosed K ∧ r < ↑↑μ K
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ InnerRegular μ IsClosed IsOpen
intro U hU r hr
case intro.intro.intro.intro
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ (n : ℕ), F n)
hr : r < ↑↑μ (⋃ (n : ℕ), F n)
⊢ ∃ K, (K ⊆ ⋃ (n : ℕ), F n) ∧ IsClosed K ∧ r < ↑↑μ K
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U✝ s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
U : Set X
hU : IsOpen U
r : ℝ≥0∞
hr : r < ↑↑μ U
⊢ ∃ K, K ⊆ U ∧ IsClosed K ∧ r < ↑↑μ K
rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩
case intro.intro.intro.intro
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ (n : ℕ), F n)
hr : r < ⨆ (i : ℕ), ↑↑μ (F i)
⊢ ∃ K, (K ⊆ ⋃ (n : ℕ), F n) ∧ IsClosed K ∧ r < ↑↑μ K
case intro.intro.intro.intro
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ (n : ℕ), F n)
hr : r < ↑↑μ (⋃ (n : ℕ), F n)
⊢ ∃ K, (K ⊆ ⋃ (n : ℕ), F n) ∧ IsClosed K ∧ r < ↑↑μ K
rw [measure_iUnion_eq_iSup F_mono.directed_le] at hr
case intro.intro.intro.intro.intro
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ (n : ℕ), F n)
hr : r < ⨆ (i : ℕ), ↑↑μ (F i)
n : ℕ
hn : r < ↑↑μ (F n)
⊢ ∃ K, (K ⊆ ⋃ (n : ℕ), F n) ∧ IsClosed K ∧ r < ↑↑μ K
case intro.intro.intro.intro
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ (n : ℕ), F n)
hr : r < ⨆ (i : ℕ), ↑↑μ (F i)
⊢ ∃ K, (K ⊆ ⋃ (n : ℕ), F n) ∧ IsClosed K ∧ r < ↑↑μ K
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
no goals
case intro.intro.intro.intro.intro
α : Type ?u.57133
β : Type ?u.57136
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝¹ : PseudoEMetricSpace X
inst✝ : MeasurableSpace X
μ : Measure X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ (n : ℕ), F n)
hr : r < ⨆ (i : ℕ), ↑↑μ (F i)
n : ℕ
hn : r < ↑↑μ (F n)
⊢ ∃ K, (K ⊆ ⋃ (n : ℕ), F n) ∧ IsClosed K ∧ r < ↑↑μ K
exact ⟨F n, subset_iUnion _ _, F_closed n, hn⟩