innerRegular_measurable — Mathlib

English

If μ is inner regular, an open cover of a compact set yields infimum of μ over open supersets.

Русский

Если μ внутри регулярна, покрытие компактного множества открытыми множествами даёт инфимуμ по открытым надмножествам.

LaTeX

$$$K\text{ compact} \Rightarrow μ(K) = \inf_{U\supset K} μ(U)\text{ with } U\text{ open}$$$

Lean4

theorem innerRegular_measurable [WeaklyRegular μ] : InnerRegularWRT μ IsClosed fun s => MeasurableSet s ∧ μ s ≠ ∞ :=
  WeaklyRegular.innerRegular.measurableSet_of_isOpen (fun _ _ h₁ h₂ ↦ h₁.inter h₂.isClosed_compl)

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