exists_isOpen_lt_add — Mathlib

English

For a compact K, for every ε>0, there exists an open set U with K ⊆ U and μ(U) < μ(K) + ε.

Русский

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

LaTeX

$$$\forall ε>0,\ \exists U\ (K\subset U)\land IsOpen(U)\land μ(U) < μ(K) + ε$$$

Lean4

protected theorem _root_.IsCompact.exists_isOpen_lt_add [InnerRegularCompactLTTop μ] [IsLocallyFiniteMeasure μ]
    [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < μ K + ε :=
  hK.exists_isOpen_lt_of_lt _ (ENNReal.lt_add_right hK.measure_lt_top.ne hε)

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