G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : ↑(Content.outerMeasure μ) ↑U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ ↑(Content.outerMeasure μ) ↑U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
rw [μ.outerMeasure_opens] at hU⊢
case intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
rcases μ.innerContent_exists_compact hU hε with ⟨K, h1K, h2K⟩
no goals
case intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ ↑(Content.outerMeasure μ) ↑K + ↑ε
exact ⟨K, h1K, le_trans h2K <| add_le_add_right (μ.le_outerMeasure_compacts K) _⟩