ContentRegular — Mathlib

English

If μ is ContentRegular, then for every compact K and every ε > 0 there exists a compact K' with K ⊆ interior(K') and μ(K') ≤ μ(K) + ε.

Русский

Если μ reguli ContentRegular, то для каждого компактного K и ε > 0 существует компактное K' с K ⊆ interior(K') и μ(K') ≤ μ(K) + ε.

LaTeX

$$$$\\forall K, ε>0,\\ \\exists K' : \\mathrm{Compacts}(G), K \\subseteq \\operatorname{int}(K') \\land μ(K') \\le μ(K) + ε.$$$$

Lean4

/-- A content `μ` is called regular if for every compact set `K`,
  `μ(K) = inf {μ(K') : K ⊂ int K' ⊂ K'}`. See Paul Halmos (1950), Measure Theory, §54. -/
def ContentRegular :=
  ∀ ⦃K : TopologicalSpace.Compacts G⦄,
    μ K = ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K'

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