exists_isClosed_lt_add — Mathlib

English

If K is compact, there exists an open U with μ(U) < μ(K) + ε for any ε>0.

Русский

Если K компактно, существует открытое U, такое что μ(U) < μ(K) + ε для любого ε>0.

LaTeX

$$$\forall ε>0:\exists U\text{ open}, K\subset U \land μ(U) < μ(K) + ε$$$

Lean4

/-- If `s` is a measurable set, a weakly regular measure `μ` is finite on `s`, and `ε` is a positive
number, then there exist a closed set `K ⊆ s` such that `μ s < μ K + ε`. -/
theorem _root_.MeasurableSet.exists_isClosed_lt_add [WeaklyRegular μ] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ K, K ⊆ s ∧ IsClosed K ∧ μ s < μ K + ε :=
  innerRegular_measurable.exists_subset_lt_add isClosed_empty ⟨hs, hμs⟩ hμs hε

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