Theorems · Theorem · general topology
Filter.tendsto_atTop_atTop_of_monotone
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → (∀ (b : β), ∃ a, b ≤ f a) → Filter.Tendsto f Filter.atTop Filter.atTop- Defined in
- Mathlib.Order.Filter.AtTopBot.Tendsto
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Set.ofPredproof · cited by 6,101
- Filter.Tendstostatement · cited by 3,814
- Filter.Eventuallyproof · cited by 3,134
- Filter.atTopstatement and proof · cited by 2,405
- Monotonestatement and proof · cited by 1,397
- Set.Iciproof · cited by 1,070
- le_transproof · cited by 985
- Filter.mem_of_supersetproof · cited by 308
- Filter.tendsto_principalproof · cited by 28
- Filter.tendsto_iInfproof · cited by 13
- Filter.mem_atTopproof · cited by 9
Cited by8
Results whose statement or proof uses this declaration.
- Monotone.tendsto_atTop_atTopproof · cited by 13
- Filter.comap_embedding_atTopproof · cited by 4
- tendsto_PNat_val_atTop_atTopproof · cited by 2
- isPowMul_smoothingFunproof · cited by 1
- seminormFromConst_const_mulproof · cited by 1
- seminormFromConst_isPowMulproof · cited by 1
- factorial_tendsto_atTopproof · cited by 0
- Filter.tendsto_atTop_atBot_of_antitoneproof · cited by 0