le_innerContent — Mathlib

English

Let μ be a content measure on G. If K is a compact subset of G and U is an open subset of G with K ⊆ U, then μ(K) ≤ μ.innerContent(U).

Русский

Пусть μ — содержательная мера на G. Пусть K — компактное подмножество G и U — открытое множество G с K ⊆ U. Тогда μ(K) ≤ μ.innerContent(U).

LaTeX

$$$\\forall K \\in \\mathrm{Compacts}(G)\\,\\forall U \\in \\mathrm{Opens}(G),\\ (K \\subseteq U) \\Rightarrow \\mu(K) \\le \\mu\\!\\cdot\\text{innerContent}(U)$$$

Lean4

theorem le_innerContent (K : Compacts G) (U : Opens G) (h2 : (K : Set G) ⊆ U) : μ K ≤ μ.innerContent U :=
  le_iSup_of_le K <| le_iSup (fun _ ↦ (μ.toFun K : ℝ≥0∞)) h2

Похожие утверждения