theorem
proved
orMethodCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.OperationsResearchFromRS on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
22 | linearProgramming | dynamicProgramming | gameTheory | queuingTheory | simulation
23 deriving DecidableEq, Repr, BEq, Fintype
24
25theorem orMethodCount : Fintype.card ORMethod = 5 := by decide
26
27/-- Optimal solution: J = 0. -/
28theorem optimal_solution : Jcost 1 = 0 := Jcost_unit0
29
30structure OperationsResearchCert where
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