Theorems · Definition · measure theory

MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq

{α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : PseudoEMetricSpace E] →
          {f : ℕ → α → E} → {g : α → E} → MeasureTheory.TendstoInMeasure μ f Filter.atTop g → ℕ → ℕ

Transformation of seqTendstoAeSeqAux to makes sure it is strictly monotone.

Defined in: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Cited by: 6 results in Mathlib
Foundations: Depth 174 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.

Cites5

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

Cited by6

Results whose statement or proof uses this declaration.

MeasureTheory.TendstoInMeasure.exists_seq_tendsto_aeproof · cited by 5
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_specstatement and proof · cited by 1
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMonostatement and proof · cited by 1
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_succstatement and proof · cited by 1
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.congr_simpstatement and proof · cited by 0
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.eq_defstatement and proof · cited by 0