Structures · Topology
BoundedAdd
A typeclass saying that (p : R × R) ↦ p.1 + p.2 maps any product of bounded sets to a bounded
set. This property follows from LipschitzAdd, and thus automatically holds, e.g., for seminormed
additive groups.
- Shape
- One type argument · adds isBounded_add
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- BoundedContinuousFunction.toContinuousMapLinearMap
- isBounded_add
- BoundedContinuousFunction.toContinuousMapAddMonoidHom
- BoundedContinuousFunction.coeFnAddMonoidHom
- BoundedContinuousFunction.coe_sum
- AddMonoidHom.compLeftContinuousBounded
- BoundedAdd.isBounded_add
- BoundedContinuousFunction.coe_nsmul
- BoundedContinuousFunction.evalCLM
- BoundedContinuousFunction.add_compContinuous
- AddMonoidHom.compLeftContinuousBounded_apply
- BoundedContinuousFunction.coeFnAddMonoidHom_apply
- BoundedContinuousFunction.toContinuousMapLinearMap_apply
- BoundedContinuousFunction.instNSMul
- BoundedContinuousFunction.toContinuousMapAddMonoidHom_apply
- add_bounded_of_bounded_of_bounded
- BoundedContinuousFunction.instAddCommMonoid
- BoundedContinuousFunction.coe_nsmulRec
- BoundedContinuousFunction.instAddMonoid
- BoundedContinuousFunction.sum_apply
- BoundedContinuousFunction.instDistribMulAction
- BoundedContinuousFunction.coe_add
- isBounded_nsmul
- BoundedContinuousFunction.instAddZeroClass
- BoundedContinuousFunction.add_apply
- BoundedContinuousFunction.mkOfCompact_add
- BoundedContinuousFunction.evalCLM_apply
- BoundedContinuousFunction.nsmul_apply
- BoundedContinuousFunction.instAdd
- BoundedContinuousFunction.instSemiring
- BoundedContinuousFunction.instModule
Ancestors0
No ancestors.