G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ ↑(toFun μ (K₁ ⊔ K₂)) ≤ ↑(toFun μ K₁) + ↑(toFun μ K₂)
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ (fun s => ↑(toFun μ s)) (K₁ ⊔ K₂) ≤ (fun s => ↑(toFun μ s)) K₁ + (fun s => ↑(toFun μ s)) K₂
simp only [apply_eq_coe_toFun]
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ toFun μ (K₁ ⊔ K₂) ≤ toFun μ K₁ + toFun μ K₂
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ ↑(toFun μ (K₁ ⊔ K₂)) ≤ ↑(toFun μ K₁) + ↑(toFun μ K₂)
norm_cast
no goals
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ toFun μ (K₁ ⊔ K₂) ≤ toFun μ K₁ + toFun μ K₂
exact μ.sup_le' _ _