Continuous Perfect Pairing for topDualPairing #
This file proves that topDualPairing 𝕜 E is a continuous perfect pairing when E is a
finite-dimensional Hausdorff space over a complete nontrivially normed field.
Main results #
topDualPairing_isContPerfPair: ThetopDualPairingis a continuous perfect pairing for finite-dimensional Hausdorff spaces over complete nontrivially normed fields.
instance
topDualPairing_isContPerfPair
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[FiniteDimensional 𝕜 E]
[T2Space E]
:
(topDualPairing 𝕜 E).IsContPerfPair
The topDualPairing is a continuous perfect pairing for finite-dimensional
Hausdorff spaces over complete nontrivially normed fields.