English
For SFinite ν, if s ⊆ (μ.sigmaFiniteSetWRT' ν)^c and ν s ≠ 0, then μ s = ∞.
Русский
Если ν SFinite, и s ⊆ (μ.sigmaFiniteSetWRT'(ν))^c, а ν(s) ≠ 0, то μ(s) = ∞.
LaTeX
$$$$\text{If } [SFinite(\nu)] \; (hs\subseteq (\mu\sigmaFiniteSetWRT'(\nu))^c) \; (\nu(s) \neq 0) \Rightarrow \mu(s)=\infty.$$$$
Lean4
/-- For all sets `s` in `(μ.sigmaFiniteSetWRT ν)ᶜ`, if `ν s ≠ 0` then `μ s = ∞`. -/
theorem measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' [IsFiniteMeasure ν]
(hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ) (hνs : ν s ≠ 0) : μ s = ∞ :=
by
rw [measure_eq_iInf]
simp_rw [iInf_eq_top]
suffices ∀ t, t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ → s ⊆ t → MeasurableSet t → μ t = ∞
by
intro t hts ht
suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from measure_mono_top Set.inter_subset_left this
have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset
exact
this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
(ht.inter measurableSet_sigmaFiniteSetWRT'.compl)
intro t ht_subset hst ht
refine measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_
exact fun hνt ↦ hνs (measure_mono_null hst hνt)
