Structures · Topology

LinearMap.IsContPerfPair

For a topological ring R and two topological modules M and N, a continuous perfect pairing is a continuous bilinear map M × N → R that is bijective in both arguments. We require continuity in the forward direction only so that we can put several different topologies on the continuous dual: strong, weak, weak-\* topology...

Defined in

Mathlib.Topology.Algebra.Module.PerfectPairing

Shape

One type argument · adds continuous_uncurry, bijective_left, bijective_right