Structures · Topology
BoundedMul
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 non-unital seminormed rings, but it also holds, e.g.,
for ℝ≥0.
- Shape
- One type argument · adds isBounded_mul
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 by22
- BoundedContinuousFunction.coe_prod
- isBounded_mul
- BoundedContinuousFunction.coeFnMonoidHom
- MonoidHom.compLeftContinuousBounded
- BoundedMul.isBounded_mul
- BoundedContinuousFunction.pow_apply
- BoundedContinuousFunction.toContinuousMapMonoidHom
- BoundedContinuousFunction.toContinuousMapMonoidHom_apply
- isBounded_pow
- BoundedContinuousFunction.coe_mul
- BoundedContinuousFunction.instPow
- BoundedContinuousFunction.instMul
- MonoidHom.compLeftContinuousBounded_apply
- mul_bounded_of_bounded_of_bounded
- BoundedContinuousFunction.instMulOneClass
- BoundedContinuousFunction.coe_pow
- BoundedContinuousFunction.prod_apply
- BoundedContinuousFunction.instMonoid
- BoundedContinuousFunction.instCommMonoid
- BoundedContinuousFunction.instSemiring
- BoundedContinuousFunction.mul_apply
- BoundedContinuousFunction.coeFnMonoidHom_apply
Ancestors0
No ancestors.