Prop. 4.0.1 — in metric spaces, sequential completeness implies completeness for nets

Proved

GarrettFA.metric_net_complete_of_seq_complete

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysistopological-vector-spaces

Let $(M,d)$ be a metric space in which every Cauchy sequence converges. Let $(v_i)_{i\in I}$ be a net indexed by a directed partially ordered set that is Cauchy for $d$ : for every $\varepsilon>0$ there is $i_0$ with $d(v_i,v_j)<\varepsilon$ for all $i,j\ge i_0$ . Then there is $x\in M$ such that

the net converges to $x$ : for every $\varepsilon>0$ there is $i_0$ with $d(v_i,x)<\varepsilon$ for all $i\ge i_0$ ; and
there is a monotone sequence of indices $i_1\le i_2\le\cdots$ with $v_{i_n}\to x$ .

Formalization Note The notes speak of "cofinal sequences converging to the same limit". A directed set need not contain a cofinal sequence, so this clause is formalized as a monotone sequence of indices along which the net converges to $x$ , which is what the proof constructs.

Preamble

import Mathlib

Formal statement

namespace GarrettFA
theorem metric_net_complete_of_seq_complete {M : Type*} [MetricSpace M]
    (hM : ∀ u : ℕ → M, CauchySeq u → ∃ x, Filter.Tendsto u Filter.atTop (nhds x))
    {I : Type*} [PartialOrder I] [IsDirected I (· ≤ ·)] (v : I → M)
    (hv : ∀ ε > 0, ∃ i₀ : I, ∀ i ≥ i₀, ∀ j ≥ i₀, dist (v i) (v j) < ε) :
    ∃ x : M, (∀ ε > 0, ∃ i₀ : I, ∀ i ≥ i₀, dist (v i) x < ε) ∧
      ∃ s : ℕ → I, Monotone s ∧ Filter.Tendsto (v ∘ s) Filter.atTop (nhds x) := by sorry
end GarrettFA

Source

Paul Garrett, *Completeness and quasi-completeness* (lecture notes, April 24, 2014), http://www.math.umn.edu/~garrett/m/fun/notes_2012-13/07d_quasi-completeness.pdf, p. 6, Proposition 4.0.1

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $M$ be a metric space with distance $d$ (no vector structure). Assume $M$ is sequentially complete: every Cauchy sequence $(u_n)_{n\in\mathbb N}$ in $M$ converges to some point of $M$ . Let $I$ be any type (any universe) with a partial order in which any two elements have a common upper bound, and let $v:I\to M$ satisfy the Cauchy condition: for every $\varepsilon>0$ there is $i_0$ with $d(v_i,v_j)<\varepsilon$ for all $i,j\ge i_0$ . Then there exists $x\in M$ such that both

for every $\varepsilon>0$ there is $i_0$ with $d(v_i,x)<\varepsilon$ for all $i\ge i_0$ (the net converges to $x$ ), and
there is a monotone sequence of indices $s:\mathbb N\to I$ ( $n\le m\Rightarrow s_n\le s_m$ ) such that $v_{s_n}\to x$ as $n\to\infty$ .

The sequence $s$ is only required to be monotone; it is not required to be cofinal in $I$ . If $I$ is empty the Cauchy hypothesis fails, so the statement is vacuous there.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph