OAI/Combinatorics/UniformKServer/FiniteLawTheorem.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-law theorem has arbitrary request atoms and literal offline OPT. Its endpoint is fixed by the instance, before the law or horizon are chosen.

  1. theorem OAI.UniformKServer.OfflineLaw.finite_law line 17