G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ False
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
by_contra hc
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
⊢ False
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ False
simp only [not_exists, not_and, not_le] at hc
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
lower_bound_iInf :
  (fun s => ↑(toFun μ s)) K + ↑ε ≤ ⨅ (K' : Compacts G) (_ : ↑K ⊆ interior ↑K'), (fun s => ↑(toFun μ s)) K'
⊢ False
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
⊢ False
have lower_bound_iInf : μ K + ε ≤
    ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K' :=
  le_iInf fun K' => le_iInf fun K'_hyp => le_of_lt (hc K' K'_hyp)
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
lower_bound_iInf : (fun s => ↑(toFun μ s)) K + ↑ε ≤ (fun s => ↑(toFun μ s)) K
⊢ False
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
lower_bound_iInf :
  (fun s => ↑(toFun μ s)) K + ↑ε ≤ ⨅ (K' : Compacts G) (_ : ↑K ⊆ interior ↑K'), (fun s => ↑(toFun μ s)) K'
⊢ False
rw [← H] at lower_bound_iInf
no goals
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(toFun μ K) + ↑ε < ↑(toFun μ x)
lower_bound_iInf : (fun s => ↑(toFun μ s)) K + ↑ε ≤ (fun s => ↑(toFun μ s)) K
⊢ False
exact (lt_self_iff_false (μ K)).mp (lt_of_le_of_lt' lower_bound_iInf
  (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))