OAI/Combinatorics/UniformKServer/TierInner.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

At a heavy request the inner ball has no short-edit error: the completed heavy key shadows every short tier, while a qualifying tier covers that ball.

  1. theorem OAI.UniformKServer.TierLabeledKeys.coverage_near line 19
  2. theorem OAI.UniformKServer.TierLabeledKeys.annular_stationary line 38
  3. theorem OAI.UniformKServer.TierLabeledKeys.annular_mover line 80