OAI/Combinatorics/ProgressionColoring/Model.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuantitativeVanDerWaerden.MonoAP line 9

   Also declared: ComparatorChallenges/QuantitativeVanDerWaerden.lean:9 (same declaration text).

2. def OAI.QuantitativeVanDerWaerden.HasMonoAP line 12

   Also declared: ComparatorChallenges/QuantitativeVanDerWaerden.lean:12 (same declaration text).

3. def OAI.QuantitativeVanDerWaerden.IsRamsey line 15

   Also declared: ComparatorChallenges/QuantitativeVanDerWaerden.lean:15 (same declaration text).

4. def OAI.QuantitativeVanDerWaerden.W line 20

   Source documentation

   The least positive Ramsey interval size. Statements about its Ramsey property require a finiteness proof; no such proof is built into this definition.

   Distinct definitions of this name: ComparatorChallenges/QuantitativeVanDerWaerden.lean:20 (same statement text; different proof or body). Qualify references as OAI.QuantitativeVanDerWaerden.W@path.

   noncomputable def W (r k : ℕ) : ℕ :=
   …