English
Let 𝕜 be a nontrivial normed field that is weakly locally compact. Then 𝕜, as a metric space, is a proper space (all closed balls are compact).
Русский
Пусть 𝕜 — ненулевое нормированное поле, обладающее слабой локальной компактностью. Тогда 𝕜 как метрическое пространство является правомерным: любая замкнутая шарa конечного радиуса компактна.
LaTeX
$$$\\text{If } 𝕜 \\\\text{is a nontrivial normed field and } 𝕜 \\\\text{is WeaklyLocallyCompact, then } 𝕜 \\\\text{is a proper metric space (all closed balls are compact).}$$$
Lean4
/-- A weakly locally compact normed field is proper.
This is a specialization of `ProperSpace.of_locallyCompactSpace`
which holds for `NormedSpace`s but requires more imports. -/
theorem of_nontriviallyNormedField_of_weaklyLocallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜]
[WeaklyLocallyCompactSpace 𝕜] : ProperSpace 𝕜 :=
by
rcases exists_isCompact_closedBall (0 : 𝕜) with ⟨r, rpos, hr⟩
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
have hC n : IsCompact (closedBall (0 : 𝕜) (‖c‖ ^ n * r)) :=
by
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
convert hr.smul (c ^ n)
ext
simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this, smul_eq_mul, norm_mul,
norm_inv, norm_pow, inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)]
have hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop :=
Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
exact .of_seq_closedBall hTop (Eventually.of_forall hC)
