Documentation
LeanPool
.
ParameterFreeGradient
.
V7
.
Proofs
.
Anchor
Search
return to top
source
Imports
Init
LeanPool.ParameterFreeGradient.O3.Stage3Anchor
LeanPool.ParameterFreeGradient.V7.Proofs.GuardAdapters
Imported by
V7
.
anchor
The anchor-search theorem transported to the current positive secant interface.
source
theorem
V7
.
anchor
:
AnchorStatement