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: The topDualPairing is 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.