exists_lt_isClosed — Mathlib

English

If K is compact, there exists an open U⊇K with μ(U) arbitrarily close to μ(K).

Русский

Если K компактно, существует открытое U ⊇ K, такое что μ(U) произвольно близко к μ(K).

LaTeX

$$$K\text{ compact} \Rightarrow ∀ε>0:\exists U\supset K,\ IsOpen(U)\land μ(U) < μ(K) + ε$$$

Lean4

/-- If `μ` is a weakly regular measure, then any open set can be approximated by a closed subset. -/
theorem _root_.IsOpen.exists_lt_isClosed [WeaklyRegular μ] ⦃U : Set α⦄ (hU : IsOpen U) {r : ℝ≥0∞} (hr : r < μ U) :
    ∃ F, F ⊆ U ∧ IsClosed F ∧ r < μ F :=
  WeaklyRegular.innerRegular hU r hr

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