Theorems · Theorem · measure theory

MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_succ

∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) {n : ℕ},
  MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg (n + 1) =
    max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1))
      (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)

Defined in: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Cited by: 1 results in Mathlib
Foundations: Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Filter.atTopstatement and proof · cited by 2,405
PseudoEMetricSpacestatement and proof · cited by 1,536
MeasureTheory.TendstoInMeasurestatement and proof · cited by 51
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqstatement and proof · cited by 6
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAuxstatement and proof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMonoproof · cited by 1