English
If a metric space α is proper (closed balls are compact), then α is complete; equivalently, every Cauchy filter on α converges.
Русский
Если метрическое пространство α является правильным (замкнутые шаровые множества компакты), то оно полно; эквивалентно тому, что любая Cauchy-фильтра на α сходится.
LaTeX
$$$\\text{ProperSpace}(\\alpha) \\Rightarrow \\text{CompleteSpace}(\\alpha)$$$
Lean4
/-- A proper space is complete -/
instance (priority := 100) complete_of_proper [ProperSpace α] : CompleteSpace α :=
⟨fun {f} hf => by
/- We want to show that the Cauchy filter `f` is converging. It suffices to find a closed
ball (therefore compact by properness) where it is nontrivial. -/
obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 := (Metric.cauchy_iff.1 hf).2 1 zero_lt_one
rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩
have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le
rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf (le_principal_iff.2 this) with
⟨y, -, hy⟩
exact ⟨y, hy⟩⟩
