OAI/Combinatorics/UniformKServer/FirstEdits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Serializing actual priority edits. The higher-priority prefix uses its new state and the lower-priority suffix its old state, exactly as in source.

  1. def OAI.UniformKServer.FirstStructure.overlayKey line 17
  2. def OAI.UniformKServer.FirstStructure.editSum line 20
  3. theorem OAI.UniformKServer.FirstStructure.indicator_triangle line 25
  4. theorem OAI.UniformKServer.FirstStructure.overlay_step line 29
  5. theorem OAI.UniformKServer.FirstStructure.serial_bound line 33
  6. theorem OAI.UniformKServer.FirstStructure.editSum_nonneg line 53