English
For a compact K and a local finite measure μ, μ(K) equals the infimum of μ(U) over open sets U containing K.
Русский
Для компактного множества K и локально конечной меры μ выполняется равенство μ(K) равному инфимума μ(U) по всем открытым U, содержащим K.
LaTeX
$$$K \text{ компакт} \Rightarrow μ(K) = \inf_{U\supset K} μ(U),\ U\text{ открыто}$$$
Lean4
/-- If `μ` is inner regular for finite measure sets with respect to compact sets
and is locally finite in an R₁ space,
then any compact set can be approximated from outside by open sets. -/
protected theorem _root_.IsCompact.measure_eq_iInf_isOpen [InnerRegularCompactLTTop μ] [IsLocallyFiniteMeasure μ]
[R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) : μ K = ⨅ (U : Set α) (_ : K ⊆ U) (_ : IsOpen U), μ U :=
by
apply le_antisymm
· simp only [le_iInf_iff]
exact fun U KU _ ↦ measure_mono KU
· apply le_of_forall_gt
simpa only [iInf_lt_iff, exists_prop, exists_and_left] using hK.exists_isOpen_lt_of_lt
