Theorems · Theorem · general topology
Filter.Tendsto.bddAbove_range
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] {a : α} [IsDirectedOrder α]
{u : ℕ → α}, Filter.Tendsto u Filter.atTop (nhds a) → BddAbove (Set.range u)- Defined in
- Mathlib.Topology.Order.LiminfLimsup
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Preorderstatement and proof · cited by 7,952
- nhdsstatement and proof · cited by 5,554
- Set.rangestatement · cited by 4,705
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.atTopstatement and proof · cited by 2,405
- BddAbovestatement · cited by 620
- IsDirectedOrderstatement and proof · cited by 316
- Filter.Tendsto.isBoundedUnder_leproof · cited by 25
- BoundedLENhdsClassstatement and proof · cited by 7
- Filter.IsBoundedUnder.bddAbove_rangeproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- IsClosed.upperClosure_piproof · cited by 2
- MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_auxproof · cited by 1