Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionComputeSiInt
Search
return to top
source
Imports
Init
Mathlib.Tactic.Common
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntGoal
Imported by
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_all
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiInt
#
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_all
(
r
:
Block
)
(
i
:
Var
)
(
p
q
:
Fin
3
)
:
SiIntGoal
r
i
p
q