OAI/Combinatorics/EditApproximation/Geometry/WideBellman.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bellman cones of the actual labeled finite wide actions preserve both lower invariants.

  1. def OAI.EditApproximation.actualWideActions line 13
  2. def OAI.EditApproximation.actualWideBellman line 19
  3. theorem OAI.EditApproximation.actual_coned_action_lower line 26
  4. theorem OAI.EditApproximation.actualWideBellman_lower line 60