Documentation
LeanPool
.
FrontierMathOpenHypergraphs
.
Uniform
.
FrameExact
Search
return to top
source
Imports
Init
LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameDefs
Imported by
HypergraphLowerBound
.
exactSmallFrames_valid
Exact small-frame validations
#
source
theorem
HypergraphLowerBound
.
exactSmallFrames_valid
(
spec
:
FrameSpec
)
:
spec
∈
exactSmallFrames
→
spec
.
IsValid