measure_eq_zero_of_subset_diff_everywherePosSubset

English

If k is compact and k ⊆ s \\ μ.everywherePosSubset s, then μ(k) = 0.

Русский

Если k компактно и k ⊆ (s \\ μ.everywherePosSubset s), то μ(k) = 0.

LaTeX

$$$$ \\text{If } k \\text{ is compact and } k \\subseteq s \\setminus μ.everywherePosSubset s, \\text{ then } μ(k)=0. $$$$

Lean4

/-- Any compact set contained in `s \ μ.everywherePosSubset s` has zero measure. -/
theorem measure_eq_zero_of_subset_diff_everywherePosSubset (hk : IsCompact k) (h'k : k ⊆ s \ μ.everywherePosSubset s) :
    μ k = 0 := by
  apply hk.induction_on (p := fun t ↦ μ t = 0)
  · exact measure_empty
  · exact fun s t hst ht ↦ measure_mono_null hst ht
  · exact fun s t hs ht ↦ measure_union_null hs ht
  · intro x hx
    obtain ⟨u, ux, hu⟩ : ∃ u ∈ 𝓝[s] x, μ u = 0 := by simpa [everywherePosSubset, (h'k hx).1] using (h'k hx).2
    exact ⟨u, nhdsWithin_mono x (h'k.trans diff_subset) ux, hu⟩

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