OAI/NumberTheory/DukePrimeDegree/Entropy/FinitePrefixChartCodes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite codes for a growing prefix of coordinate charts

The label records chart membership as well as the coordinate grid. A single sufficiently advanced label therefore resolves any fixed chart.

  1. theorem OAI.DukePrimeDegree.exists_finite_prefix_chart_codes line 15