Theorems · Inductive type · general topology
BoundedLENhdsClass
(α : Type u_7) → [Preorder α] → [TopologicalSpace α] → Prop
Ad hoc typeclass stating that neighborhoods are eventually bounded above.
- Defined in
- Mathlib.Topology.Order.LiminfLimsup
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- PreorderTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- Preorderstatement · cited by 7,952
Cited by9
Results whose statement or proof uses this declaration.
- Filter.Tendsto.isBoundedUnder_lestatement and proof · cited by 25
- isBounded_le_nhdsstatement and proof · cited by 4
- Filter.Tendsto.bddAbove_range_of_cofinitestatement and proof · cited by 3
- Filter.Tendsto.bddAbove_rangestatement and proof · cited by 2
- BoundedLENhdsClass.isBounded_le_nhdsstatement and proof · cited by 1
- isCobounded_ge_nhdsstatement and proof · cited by 0
- Filter.Tendsto.isCoboundedUnder_gestatement and proof · cited by 0
- BoundedLENhdsClass.casesOnstatement and proof · cited by 0
- BoundedLENhdsClass.recOnstatement and proof · cited by 0