Documentation
LeanPool
.
FrontierMathOpenHypergraphs
.
Uniform
.
FrameResidues
Search
return to top
source
Imports
Init
LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameDefs
Imported by
HypergraphLowerBound
.
residueGadgets_valid
Residue-gadget validations
#
source
theorem
HypergraphLowerBound
.
residueGadgets_valid
(
spec
:
FrameSpec
)
:
spec
∈
residueGadgets
→
spec
.
IsValid