English
If K is compact and μ(K) < r, then there exists an open set U with K ⊆ U and μ(U) < r.
Русский
Если K компактно и μ(K) < r, существует открытое множество U с K ⊆ U и μ(U) < r.
LaTeX
$$$\text{IsCompact}(K) \Rightarrow (\exists U\; K \subset U \land \text{IsOpen}(U) \land μ(U) < r)$$$
Lean4
protected theorem _root_.IsCompact.exists_isOpen_lt_of_lt [InnerRegularCompactLTTop μ] [IsLocallyFiniteMeasure μ]
[R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) (r : ℝ≥0∞) (hr : μ K < r) :
∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r :=
by
rcases hK.exists_open_superset_measure_lt_top μ with ⟨V, hKV, hVo, hμV⟩
have := Fact.mk hμV
obtain ⟨U, hKU, hUo, hμU⟩ : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ.restrict V U < r :=
exists_isOpen_lt_of_lt K r <| (restrict_apply_le _ _).trans_lt hr
refine ⟨U ∩ V, subset_inter hKU hKV, hUo.inter hVo, ?_⟩
rwa [restrict_apply hUo.measurableSet] at hμU
