Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionComputeS0IntBlock1
Search
return to top
source
Imports
Init
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntGoal
Mathlib.Tactic.Positivity.Finset
Imported by
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
s0IntGoal_block1
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock1
#
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
s0IntGoal_block1
(
p
q
:
Fin
3
)
:
S0IntGoal
⟨
1
,
s0IntGoal_block1._proof_1
⟩
p
q