English
Every nontrivial normed module over a nontrivial normed field is a perfect space.
Русский
Любое ненулевое нормированное модуль над ненулевым нормированным полем является совершенным пространством.
LaTeX
$$$\text{PerfectSpace } E\quad\text{for } E\text{ a nontrivial normed module over } 𝕜.$$$
Lean4
theorem perfectSpace_of_module : PerfectSpace E :=
by
refine ⟨fun x hx ↦ ?_⟩
let ⟨r, hr₀, hr⟩ := NormedField.exists_norm_lt_one 𝕜
obtain ⟨c, hc⟩ : ∃ (c : E), c ≠ 0 := exists_ne 0
have A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + (0 : 𝕜) • c)) :=
by
apply Tendsto.add tendsto_const_nhds
exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).smul tendsto_const_nhds
have B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ { x }] x) :=
by
simp only [zero_smul, add_zero] at A
simp [tendsto_nhdsWithin_iff, A, hc, norm_pos_iff.mp hr₀]
exact accPt_principal_iff_nhdsWithin.mpr ((atTop_neBot.map _).mono B)
