Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000MaskComplete

LeanPool.TwoColoringOneRound.LowerBound.N1000000MaskComplete #

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000MaskComplete.Mask :
Type

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

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

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

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Distributed2Coloring.LowerBound.N1000000MaskComplete.instDecidablePredMaskIsPartialPermMask :
      DecidablePred IsPartialPermMask
      Equations
      source
      def Distributed2Coloring.LowerBound.N1000000MaskComplete.partialPermMasks :
      Finset Mask

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

      Equations
      Instances For
        source
        theorem Distributed2Coloring.LowerBound.N1000000MaskComplete.mem_masks_toFinset_of_isPartialPermMask {m : Mask} (hm : m < 1 <<< 9) (hperm : IsPartialPermMask m) :
        m ∈ N1000000Witness.masks.toList.toFinset
        source
        theorem Distributed2Coloring.LowerBound.N1000000MaskComplete.maskAt_injective :
        Function.Injective N1000000StructureConstants.maskAt
        source
        theorem Distributed2Coloring.LowerBound.N1000000MaskComplete.exists_dirIdx_of_isPartialPermMask {m : Mask} (hm : m < 1 <<< 9) (hperm : IsPartialPermMask m) :
        ∃ (d : DirIdx), N1000000StructureConstants.maskAt d = m