Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionComputeSiIntBlock2Vars16to19
Search
return to top
source
Imports
Init
Mathlib.Tactic.Common
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntGoal
Imported by
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var16
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var17
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var18
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars16to19
#
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var16
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
2
,
⋯
⟩
⟨
16
,
⋯
⟩
p
q
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var17
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
2
,
⋯
⟩
⟨
17
,
⋯
⟩
p
q
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var18
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
2
,
⋯
⟩
⟨
18
,
⋯
⟩
p
q
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block2_var19
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
2
,
⋯
⟩
⟨
19
,
⋯
⟩
p
q