Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} (𝕜 : Type u_3) [inst_3 : RCLike 𝕜] {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω}
  {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω 𝕜),
      Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

1 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceRCLike