OAI/NumberTheory/DukePrimeDegree/Entropy/CountableSparseFineObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One low-entropy observation for a countable coordinate atlas

  1. theorem OAI.DukePrimeDegree.exists_countable_sparse_fine_observation line 17