English
Let K be a normed field. Then K is a complete metric space if and only if the closed unit ball centered at 0, i.e. {z ∈ K : ∥z∥ ≤ 1}, is complete.
Русский
Пусть K — нормированное поле. Тогда K является полным метрическим пространством тогда и только тогда, когда замкнутый шар единицы с центром в 0, то есть {z ∈ K : ∥z∥ ≤ 1}, полон.
LaTeX
$$$\\mathrm{CompleteSpace}(K) \\iff \\mathrm{IsComplete}(\\operatorname{Metric.closedBall}(0,1) : \\mathrm{Set}\,K)$$$
Lean4
theorem completeSpace_iff_isComplete_closedBall {K : Type*} [NormedField K] :
CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1 : Set K) :=
by
constructor <;> intro h
· exact Metric.isClosed_closedBall.isComplete
rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _ | ⟨_, rfl⟩
· rwa [completeSpace_iff_isComplete_univ, ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]
refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
obtain ⟨k, hk⟩ := hu.norm_bddAbove
have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k
have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 :=
by
intro
simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
rw [div_le_one (kpos.trans_lt hx)]
exact hx.le.trans' (hk (by simp))
obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
refine ⟨a * x, (((continuous_mul_right x).tendsto a).comp ha').congr ?_⟩
have hx' : x ≠ 0 := by
contrapose! hx
simp [hx, kpos]
simp [div_mul_cancel₀ _ hx']
