OAI/Combinatorics/UniformKServer/CausalSchedules.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Prefix extensionality of the concrete epoch recurrences. This supplies filtration measurability without making future parameters available early.

  1. theorem OAI.UniformKServer.CausalSchedules.active_congr line 15
  2. theorem OAI.UniformKServer.CausalSchedules.held_congr line 23
  3. theorem OAI.UniformKServer.CausalSchedules.forced_congr line 31
  4. theorem OAI.UniformKServer.CausalSchedules.epoch_congr line 40
  5. theorem OAI.UniformKServer.CausalSchedules.side_congr line 49
  6. theorem OAI.UniformKServer.CausalSchedules.reset_congr line 54
  7. theorem OAI.UniformKServer.CausalSchedules.side_reference_congr line 61
  8. theorem OAI.UniformKServer.CausalSchedules.alpha_congr line 70