def
definition
operationsResearchCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.OperationsResearchFromRS on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
31 five_methods : Fintype.card ORMethod = 5
32 optimal : Jcost 1 = 0
33
34def operationsResearchCert : OperationsResearchCert where
35 five_methods := orMethodCount
36 optimal := optimal_solution
37
38end IndisputableMonolith.Mathematics.OperationsResearchFromRS