Theorems · Theorem · measure theory

MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.congr_simp

∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  [inst : PseudoEMetricSpace E] {f f_1 : ℕ → α → E} (e_f : f = f_1) {g g_1 : α → E} (e_g : g = g_1)
  (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (a a_1 : ℕ),
  a = a_1 →
    MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg a = MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq ⋯ a_1

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

Cites6

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.