22. Topological vector spaces🔗

We describe Mathlib's theory of topological vector spaces in the sections below. The theory supports a broad class of coefficients, including ℝ, ℂ, ℚ_p (the p-adics).

1. 22.1. General topological vector spaces
2. 22.2. Locally convex spaces
3. 22.3. Banach and Hilbert spaces
4. 22.4. Continuous linear maps