Proper nontrivially normed fields

Nontrivially normed fields are ProperSpaces when they are WeaklyLocallyCompact.

Main results

• ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace

Implementation details

This is a special case of ProperSpace.of_locallyCompactSpace from Mathlib/Analysis/Normed/Module/FiniteDimension.lean, specialized to be on the field itself with a proof that requires fewer imports.

theorem ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] [WeaklyLocallyCompactSpace 𝕜] : ProperSpace 𝕜

A weakly locally compact normed field is proper. This is a specialization of ProperSpace.of_locallyCompactSpace which holds for NormedSpaces but requires more imports.