OAI/Combinatorics/ProgressionColoring/TernarySign.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ternary real comparisons, shared independently of arrangement counting.

  1. def OAI.QuantitativeVanDerWaerden.ternarySign line 13

    Source documentation

    Literal signs: 0 is negative, 1 is zero, and 2 is positive.

    def ternarySign (x : ℝ) : Fin 3 :=
…
  2. theorem OAI.QuantitativeVanDerWaerden.ternarySign_eq_zero line 16
  3. theorem OAI.QuantitativeVanDerWaerden.ternarySign_eq_one line 22
  4. theorem OAI.QuantitativeVanDerWaerden.ternarySign_eq_two line 28