OAI/Combinatorics/ProgressionColoring/MeshPartitions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuantitativeVanDerWaerden.uniformPartition line 12

   Source documentation

   The actual uniform mesh, with no extra partition hypothesis.

   def uniformPartition (n : ℕ) (hn : 0 < n) : CirclePartition (Fin n) where
   …

   Mentions: OAI.QuantitativeVanDerWaerden.CirclePartition

2. theorem OAI.QuantitativeVanDerWaerden.uniformPartition_label line 20
3. def OAI.QuantitativeVanDerWaerden.adaptivePartition line 27

   Source documentation

   The actual centered adaptive mesh, translated to the shared fundamental interval. This is a translation of cells, not an identification of labels.

   def adaptivePartition (A : AdaptiveMesh) : CirclePartition A.Label where
   …

   Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CirclePartition

4. theorem OAI.QuantitativeVanDerWaerden.adaptivePartition_label line 50