OAI/Combinatorics/UniformKServer/FirstStructure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Precedence across heavy balls, chronological tiers, and singleton fallback. A qualifying prefix covers the request, so fallback does not contribute to the short-edge separation estimate.

  1. def OAI.UniformKServer.FirstStructure.first line 16
  2. def OAI.UniformKServer.FirstStructure.key line 20
  3. def OAI.UniformKServer.FirstStructure.indicator line 22
  4. theorem OAI.UniformKServer.FirstStructure.indicator_bounds line 24
  5. theorem OAI.UniformKServer.FirstStructure.first_append line 28
  6. theorem OAI.UniformKServer.FirstStructure.first_eq_some line 36
  7. theorem OAI.UniformKServer.FirstStructure.equal_covered_prefix line 52
  8. theorem OAI.UniformKServer.FirstStructure.covered_prefix_bound line 64
  9. theorem OAI.UniformKServer.FirstStructure.indicator_map line 84