tendsto_measure_iUnion_accumulate

English

Two finite measures are equal if they agree on all measurable sets.

Русский

Две конечные меры равны, если они совпадают на всех измеримых множествах.

LaTeX

$$μ = ν if ∀ s, MeasurableSet s → (μ : Measure Ω) s = (ν : Measure Ω) s$$

Lean4

/-- Continuity from below: the measure of the union of a sequence of (not necessarily measurable)
sets is the limit of the measures of the partial unions. -/
protected theorem tendsto_measure_iUnion_accumulate {ι : Type*} [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)]
    {μ : FiniteMeasure Ω} {f : ι → Set Ω} : Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
  simpa [← ennreal_coeFn_eq_coeFn_toMeasure] using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure) (ι := ι)

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