English
If s is compact and μ is finite at every nhds of points in s, then s has an open superset U with μ(U) < ∞.
Русский
Если s компактно и для всех x ∈ s мера μ конечна в окрестности x, то существует открытое надмножество U, содержащее s, такое что μ(U) < ∞.
LaTeX
$$$$\text{If } s \text{ is compact and } \forall x \in s,\; \mu(\mathcal{N}(x)) < \infty, \text{ then } \exists U \supseteq s, \text{IsOpen}(U) \land \mu(U) < \infty.$$$$
Lean4
/-- If `s` is a compact set and `μ` is finite at `𝓝 x` for every `x ∈ s`, then `s` admits an open
superset of finite measure. -/
theorem exists_open_superset_measure_lt_top' (h : IsCompact s) (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)) :
∃ U ⊇ s, IsOpen U ∧ μ U < ∞ := by
refine IsCompact.induction_on h ?_ ?_ ?_ ?_
· use ∅
simp [Superset]
· rintro s t hst ⟨U, htU, hUo, hU⟩
exact ⟨U, hst.trans htU, hUo, hU⟩
· rintro s t ⟨U, hsU, hUo, hU⟩ ⟨V, htV, hVo, hV⟩
refine
⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
(measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩
· intro x hx
rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩
exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩
