Skip to content

Tracking: Bonnet–Myers theorem #2

Description

@AxelDlv00

Umbrella / tracking issue for the Bonnet–Myers milestone.

Bounded-below Ricci curvature on a complete Riemannian manifold ⇒ compactness + diameter bound (via the second variation of arc length).

  • This issue tracks the milestone as a whole; open sub-issues for individual lemmas/defs and link them here.
  • Claim a piece by assigning yourself to its sub-issue and moving it to In Progress on the project board.
  • The blueprint webpage remains the source of truth for math state; this board only tracks who is actively working on what.

Sources: see the book: labels.

Metadata

Metadata

Assignees

Labels

book: DoCarmoCites/formalizes from DoCarmobook: LeeRiemannianCites/formalizes from LeeRiemannianbook: PetersenCites/formalizes from Petersennot-readyHeld for human review before agent use

Type

No type

Projects

No projects

Relationships

None yet

Development

No branches or pull requests

Issue actions