OAI/Combinatorics/ProgressionColoring/OuterChoiceDefinitions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice line 15

   Source documentation

   A concrete outer coloring, with its counted family of actual cyclic words. The family is retained so that its membership proof can be used directly by the subsequent progression dichotomy.

   structure OuterChoice {k : ℕ} (s : Data k) (hk : 3 ≤ k) where
   …

   Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data