α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ InnerRegular μ IsCompact IsClosed
intro F hF r hr
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
set B : ℕ → Set X := compactCovering X
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
have hBc : ∀ n, IsCompact (F ∩ B n) := fun n => (isCompact_compactCovering X n).inter_left hF
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
have hBU : (⋃ n, F ∩ B n) = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
this : ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
have : μ F = ⨆ n, μ (F ∩ B n) := by
  rw [← measure_iUnion_eq_iSup, hBU]
  exact Monotone.directed_le fun m n h => inter_subset_inter_right _ (compactCovering_subset _ h)
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
this : ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
this : ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
rw [this] at hr
case intro
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
this : ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
n : ℕ
hn : r < ↑↑μ (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
this : ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
no goals
case intro
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
this : ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
n : ℕ
hn : r < ↑↑μ (F ∩ B n)
⊢ ∃ K, K ⊆ F ∧ IsCompact K ∧ r < ↑↑μ K
exact ⟨_, inter_subset_left _ _, hBc n, hn⟩
no goals
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ (⋃ (n : ℕ), F ∩ B n) = F
rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => F ∩ B n
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
⊢ ↑↑μ F = ⨆ (n : ℕ), ↑↑μ (F ∩ B n)
rw [← measure_iUnion_eq_iSup, hBU]
no goals
α : Type ?u.57900
β : Type ?u.57903
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ✝ : Measure α
p q : Set α → Prop
U s : Set α
ε r✝ : ℝ≥0∞
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < ↑↑μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : (⋃ (n : ℕ), F ∩ B n) = F
⊢ Directed (fun x x_1 => x ⊆ x_1) fun n => F ∩ B n
exact Monotone.directed_le fun m n h => inter_subset_inter_right _ (compactCovering_subset _ h)