Continuous linear maps on products and Pi types #
Properties that hold for non-necessarily commutative semirings. #
The cartesian product of two bounded linear maps, as a bounded linear map.
Equations
Instances For
The left injection into a product is a continuous linear map.
Equations
Instances For
The right injection into a product is a continuous linear map.
Equations
Instances For
Prod.fst
as a ContinuousLinearMap
.
Equations
Instances For
Prod.snd
as a ContinuousLinearMap
.
Equations
Instances For
Prod.map
of two continuous linear maps.
Equations
Instances For
pi
construction for continuous linear functions. From a family of continuous linear functions
it produces a continuous linear function into a family of topological modules.
Equations
Instances For
The projections from a family of topological modules are continuous linear maps.
Equations
Instances For
Given a function f : α → ι
, it induces a continuous linear function by right composition on
product types. For f = Subtype.val
, this corresponds to forgetting some set of variables.
Equations
Instances For
Pi.single
as a bundled continuous linear map.
Equations
Instances For
ContinuousLinearMap.prod
as an Equiv
.
Equations
Instances For
ContinuousLinearMap.prod
as a LinearEquiv
.
Equations
Instances For
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y
.
Equations
Instances For
Taking the product of two maps with the same codomain is equivalent to taking the product of
their domains.
See note [bundled maps over different rings] for why separate R
and S
semirings are used.
TODO: Upgrade this to a ContinuousLinearEquiv
. This should be true for any topological
vector space over a normed field thanks to ContinuousLinearMap.precomp
and
ContinuousLinearMap.postcomp
.