G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
have h'ε := ENNReal.coe_ne_zero.2 hε
case inl
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : innerContent μ U ≤ ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε

case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
cases' le_or_lt (μ.innerContent U) ε with h h
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
have h₂ := ENNReal.sub_lt_self hU h.ne_bot h'ε
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < ⨆ (K : Compacts G) (_ : ↑K ⊆ ↑U), (fun s => ↑(toFun μ s)) K
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < innerContent μ U
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
conv at h₂ => rhs; rw [innerContent]
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : ∃ i i_1, innerContent μ U - ↑ε < ↑(toFun μ i)
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : innerContent μ U - ↑ε < ⨆ (K : Compacts G) (_ : ↑K ⊆ ↑U), (fun s => ↑(toFun μ s)) K
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
simp only [lt_iSup_iff] at h₂
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ ∃ K, ↑K ⊆ ↑U✝ ∧ innerContent μ U✝ ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U
h₂ : ∃ i i_1, innerContent μ U - ↑ε < ↑(toFun μ i)
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
rcases h₂ with ⟨U, h1U, h2U⟩
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ innerContent μ U✝ ≤ (fun s => ↑(toFun μ s)) U + ↑ε
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ ∃ K, ↑K ⊆ ↑U✝ ∧ innerContent μ U✝ ≤ (fun s => ↑(toFun μ s)) K + ↑ε
refine' ⟨U, h1U, _⟩
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ innerContent μ U✝ - ↑ε ≤ (fun s => ↑(toFun μ s)) U
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ innerContent μ U✝ ≤ (fun s => ↑(toFun μ s)) U + ↑ε
rw [← tsub_le_iff_right]
no goals
case inr.intro.intro
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : innerContent μ U✝ ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < innerContent μ U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : innerContent μ U✝ - ↑ε < ↑(toFun μ U)
⊢ innerContent μ U✝ - ↑ε ≤ (fun s => ↑(toFun μ s)) U
exact le_of_lt h2U
no goals
case inl
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : innerContent μ U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : innerContent μ U ≤ ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ innerContent μ U ≤ (fun s => ↑(toFun μ s)) K + ↑ε
exact ⟨⊥, empty_subset _, le_add_left h⟩