Commit 2024-04-08 02:01 ea26fdaf

feat(Topology/Algebra/Module/WeakDual): prove basic relations between the weak topology and the original topology (#11566) (This PR continues #11472) Prove the following basic facts about the weak topology in a topological vector space (or AddCommMonoid) E.

• any set that is open in the weak topology is open in the original topology.
• any function in E that converges to a point in the original topology (with respect to some filter) converges also in the weak topology.
• if a function in E converges to a point in the original topology, then its composition with a continuous linear functional converges.
• any function from E that is continuous in the weak topology is also continuous in the original topology. Motivation: WeakSpace has some basic properties, analogue of which are proved for WeakDual. I have some doubts:
• in order to avoid typeclass instance problem, I had to add a type ascription continuousLinearMapToWeakSpace : E →L[𝕜] WeakSpace 𝕜 E when needed. Is this fine or is there a canonical way to avoid it? (I tried to add variable (𝕜 E) in before def/thm but it gave type mismatch in many places)
• I made two theorems about IsOpen, but not sure about the naming convention.