OAI/Combinatorics/UniformKServer/HeavyKeyGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Heavy precedence, disjoint nearby anchors, and the actual inner ball.

  1. theorem OAI.UniformKServer.LevelMap.Data.key_heavy_iff line 16
  2. theorem OAI.UniformKServer.LevelMap.Data.near_unique line 31
  3. theorem OAI.UniformKServer.LevelMap.Data.inner_heavy line 42