outerMeasure_interior_compacts — Mathlib

English

For every compact K in G, the outer measure of the interior of K is no larger than μ(K).

Русский

Для каждого компактного множества K в G внешний размер (outer measure) interior(K) не превосходит μ(K).

LaTeX

$$$$\\forall K \\in \\mathrm{Compacts}(G):\\mu.outerMeasure(\\operatorname{interior}K) \\le \\mu(K).$$$$

Lean4

theorem outerMeasure_interior_compacts (K : Compacts G) : μ.outerMeasure (interior K) ≤ μ K :=
  (μ.outerMeasure_opens <| Opens.interior K).le.trans <| μ.innerContent_le _ _ interior_subset

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