Theorems · Theorem · measure theory

MeasureTheory.Egorov.measure_iUnionNotConvergentSeq

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  μ (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg) ≤ ENNReal.ofReal ε

Defined in

Mathlib.MeasureTheory.Function.Egorov

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceSemilatticeSupNonemptyCountable