G : Type w
inst✝ : TopologicalSpace G
μ : Content G
this : Disjoint ↑⊥ ↑⊥ → toFun μ (⊥ ⊔ ⊥) = toFun μ ⊥ + toFun μ ⊥
⊢ (fun s => ↑(toFun μ s)) ⊥ = 0
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ (fun s => ↑(toFun μ s)) ⊥ = 0
have := μ.sup_disjoint' ⊥ ⊥
no goals
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
this : Disjoint ↑⊥ ↑⊥ → toFun μ (⊥ ⊔ ⊥) = toFun μ ⊥ + toFun μ ⊥
⊢ (fun s => ↑(toFun μ s)) ⊥ = 0
simpa [apply_eq_coe_toFun] using this