exists_open_superset_measure_lt_top

English

If s is compact and μ is locally finite, then there exists an open superset U of s with μ(U) < ∞.

Русский

Если s компактно и μ локально конечна, то существует открытое надмножество U, содержащее s, такое что μ(U) < ∞.

LaTeX

$$$$\text{If } s \text{ is compact and } \text{IsLocallyFiniteMeasure}(\mu), \exists U \supseteq s, \text{IsOpen}(U) \land \mu(U) < \infty.$$$$

Lean4

/-- If `s` is a compact set and `μ` is a locally finite measure, then `s` admits an open superset of
finite measure. -/
theorem exists_open_superset_measure_lt_top (h : IsCompact s) (μ : Measure α) [IsLocallyFiniteMeasure μ] :
    ∃ U ⊇ s, IsOpen U ∧ μ U < ∞ :=
  h.exists_open_superset_measure_lt_top' fun x _ => μ.finiteAt_nhds x

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