Registry · Proposition II.P17 tau-effective formalized

II.P17 — Geodesic Completeness

Every geodesic in Z/M_k Z can be extended indefinitely: the space is compact and complete at every finite stage.

Book II Part 10 Ch. 55

Dependency Graph

Depends on (1)

II.D81

Lean Formalization

Module: TauLib.BookII.Closure.Curvature

Symbol: geodesic_complete_2