Structures · Topology
BoundedSub
A typeclass saying that (p : R × R) ↦ p.1 - p.2 maps any product of bounded sets to a bounded
set. This property automatically holds for seminormed additive groups, but it also holds, e.g.,
for ℝ≥0.
- Shape
- One type argument · adds isBounded_sub
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- NNReal
How is a type an instance?
Loading the hierarchy index…
Assumed by6
Ancestors0
No ancestors.