English
For any ν finite, if s ⊆ (μ.sigmaFiniteSetWRT ν)^c, then μ s is either 0 or ∞ when ν s ≠ 0 implies ∞.
Русский
Для любых ν конечной, если s ⊆ (μ.sigmaFiniteSetWRT ν)^c, то μ(s) ∈ {0, ∞; и если ν(s) ≠ 0, то μ(s)=∞}.
LaTeX
$$$$\forall s,\ MeasurableSet(s)\Rightarrow s\subseteq (\mu\sigmaFiniteSetWRT(ν))^c \Rightarrow (ν(s)\neq 0 \Rightarrow μ(s)=∞).$$$$
Lean4
/-- For all sets `s` in `(μ.sigmaFiniteSetWRT ν)ᶜ`, if `ν s ≠ 0` then `μ s = ∞`. -/
theorem measure_eq_top_of_subset_compl_sigmaFiniteSetWRT [SFinite ν] (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ)
(hνs : ν s ≠ 0) : μ s = ∞ :=
by
have ⟨ν', hν', hνν', _⟩ := exists_isFiniteMeasure_absolutelyContinuous ν
have h : ∃ s : Set α, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ (∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞) :=
by
refine
⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT', sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩
exact fun hν't ↦ hνt (hνν' hν't)
rw [Measure.sigmaFiniteSetWRT, dif_pos h] at hs_subset
exact h.choose_spec.2.2 s hs_subset hνs
