G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ ≤ 0
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ = 0
refine' le_antisymm _ (zero_le _)
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ ≤ (fun s => ↑(toFun μ s)) ⊥
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ ≤ 0
rw [← μ.empty]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ (fun s => ↑(toFun μ s)) K ≤ (fun s => ↑(toFun μ s)) ⊥
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ innerContent μ ⊥ ≤ (fun s => ↑(toFun μ s)) ⊥
refine' iSup₂_le fun K hK => _
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ (fun s => ↑(toFun μ s)) K ≤ (fun s => ↑(toFun μ s)) ⊥
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ (fun s => ↑(toFun μ s)) K ≤ (fun s => ↑(toFun μ s)) ⊥
have : K = ⊥ := by
  ext1
  rw [subset_empty_iff.mp hK, Compacts.coe_bot]
no goals
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ (fun s => ↑(toFun μ s)) K ≤ (fun s => ↑(toFun μ s)) ⊥
rw [this]
case h
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ K = ⊥
ext1
no goals
case h
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥
rw [subset_empty_iff.mp hK, Compacts.coe_bot]