Mathlib Map

Structures · Topology

BoundedLENhdsClass

Ad hoc typeclass stating that neighborhoods are eventually bounded above.

Defined in
Mathlib.Topology.Order.LiminfLimsup
Shape
One type argument · adds isBounded_le_nhds

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances2

  • Prod
  • OrderDual

How is a type an instance?

Loading the hierarchy index…

Assumed by10

Ancestors0

No ancestors.