of_eq_top_imp_eq_top — Mathlib

English

If μ' and μ agree on all sets where μ is infinite, FinMeasAdditive with μ transfers to μ'.

Русский

Если μ' и μ согласуются на всех множестве, где μ бесконечна, то FinMeasAdditive переносится с μ на μ'.

LaTeX

$$FinMeasAdditive μ T → (∀s, MeasurableSet s → μ s = ∞ → μ' s = ∞) → FinMeasAdditive μ' T$$

Lean4

theorem of_eq_top_imp_eq_top {μ' : Measure α} (h : ∀ s, MeasurableSet s → μ s = ∞ → μ' s = ∞)
    (hT : FinMeasAdditive μ T) : FinMeasAdditive μ' T := fun s t hs ht hμ's hμ't hst =>
  hT s t hs ht (mt (h s hs) hμ's) (mt (h t ht) hμ't) hst

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