measure_eq_iSup_isCompact — Mathlib

English

For a regular measure μ, the measure of an open set U equals the supremum of the measures of compact subsets of U:\nμ(U) = sup{ μ(K) : K ⊆ U, K is compact }.

Русский

Для регулярной меры μ мера открытого множества U равна верхней границе мер компактных подмножества K ⊆ U:

LaTeX

$$$\\mu(U) = \\sup\\{\\mu(K) : K \\subseteq U \\text{ and } \\operatorname{IsCompact}(K)\\}$$$

Lean4

/-- The measure of an open set is the supremum of the measures of compact sets it contains. -/
theorem _root_.IsOpen.measure_eq_iSup_isCompact ⦃U : Set α⦄ (hU : IsOpen U) (μ : Measure α) [Regular μ] :
    μ U = ⨆ (K : Set α) (_ : K ⊆ U) (_ : IsCompact K), μ K :=
  Regular.innerRegular.measure_eq_iSup hU

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