Theorems · Theorem · general topology
StrictMono.tendsto_atTop
∀ {φ : ℕ → ℕ}, StrictMono φ → Filter.Tendsto φ Filter.atTop Filter.atTop- Defined in
- Mathlib.Order.Filter.AtTopBot.Tendsto
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- StrictMonostatement and proof · cited by 706
- Filter.tendsto_idproof · cited by 180
- Filter.tendsto_atTop_monoproof · cited by 22
- StrictMono.id_leproof · cited by 14
Cited by20
Results whose statement or proof uses this declaration.
- MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'proof · cited by 5
- IsLUB.exists_seq_strictMono_tendsto_of_notMemproof · cited by 4
- Besicovitch.exists_goodδproof · cited by 3
- Filter.subseq_tendsto_of_neBotproof · cited by 2
- IsClosed.upperClosure_piproof · cited by 2
- controlled_sum_of_mem_closureproof · cited by 2
- IsClosed.lowerClosure_piproof · cited by 2
- NormedAddCommGroup.completeSpace_of_summable_imp_tendstoproof · cited by 1
- Filter.HasAntitoneBasis.comp_strictMonoproof · cited by 1
- ENNReal.le_tsum_schlomilchproof · cited by 1
- IsSeqCompact.exists_tendsto_of_frequently_memproof · cited by 1
- IsSeqCompact.isCountablyCompactproof · cited by 1