19.5. Notable results
The following are some notable results in Mathlib's theory library of topological vector spaces:
-
The Open Mapping Theorem:
ContinuousLinearMap.isOpenMap -
The Hahn-Banach Theorem:
exists_extension_norm_eq -
The Lax-Milgram theorem:
IsCoercive.continuousLinearEquivOfBilin -
The Banach-Steinhaus theorem:
banach_steinhaus