Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000AvailFrom

LeanPool.TwoColoringOneRound.LowerBound.N1000000AvailFrom #

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000AvailFrom.n :
ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Distributed2Coloring.LowerBound.N1000000AvailFrom.SymN :
    Type

    Imported auxiliary declaration for the 2-coloring one-round formalization.

    Equations
    Instances For
      source
      def Distributed2Coloring.LowerBound.N1000000AvailFrom.AvailFrom (s : ℕ) :
      Type

      Symbols ≥ s inside Fin n.

      Equations
      Instances For
        source
        @[implicit_reducible]
        noncomputable instance Distributed2Coloring.LowerBound.N1000000AvailFrom.instFintypeAvailFrom (s : ℕ) :
        Fintype (AvailFrom s)
        Equations
        source
        theorem Distributed2Coloring.LowerBound.N1000000AvailFrom.card_availFrom (s : ℕ) :
        Fintype.card (AvailFrom s) = n - s