measure_eq_iSup_isClosed — Mathlib

English

For an open set U, there exists a closed F ⊆ U with μ(F) close to μ(U).

Русский

Для открытого множества U существует заполнение F ⊆ U, где μ(F) близко к μ(U).

LaTeX

$$$U\text{ open} \Rightarrow ∃F\subset U,\ IsClosed F \land μ(F) \approx μ(U)$$$

Lean4

/-- If `μ` is a weakly regular measure, then any open set can be approximated by a closed subset. -/
theorem _root_.IsOpen.measure_eq_iSup_isClosed ⦃U : Set α⦄ (hU : IsOpen U) (μ : Measure α) [WeaklyRegular μ] :
    μ U = ⨆ (F) (_ : F ⊆ U) (_ : IsClosed F), μ F :=
  WeaklyRegular.innerRegular.measure_eq_iSup hU

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