Theorems · Theorem · general topology
Monotone.tendsto_atTop_atTop
∀ {α : 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.atTopAlias of Filter.tendsto_atTop_atTop_of_monotone.
- Defined in
- Mathlib.Order.Filter.AtTopBot.Tendsto
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Quot.sound
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.
- Preorderstatement · cited by 7,952
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- Monotonestatement · cited by 1,397
- Filter.tendsto_atTop_atTop_of_monotoneproof · cited by 8
Cited by13
Results whose statement or proof uses this declaration.
- tendsto_natCast_atTop_atTopproof · cited by 51
- Filter.tendsto_finset_rangeproof · cited by 15
- tendsto_atTop_isLUBproof · cited by 7
- tendsto_nat_floor_atTopproof · cited by 6
- Filter.tendsto_atTop_atTop_of_monotone'proof · cited by 5
- Filter.map_atTop_eq_of_gc_preorderproof · cited by 3
- tendsto_pow_atTop_nhds_zero_iffproof · cited by 2
- Filter.tendsto_finsetProd_atTopproof · cited by 2
- tendsto_floor_atTopproof · cited by 1
- Filter.tendsto_atTop_of_monotone_of_filterproof · cited by 1
- tendsto_nat_ceil_atTopproof · cited by 1
- tendsto_ceil_atTopproof · cited by 0