OAI/Geometry/HyperbolicGroups/RelativeSmallPartition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.uniform_small_interior_partition line 18

   Source documentation

   The random-data-independent cutoff for literal small interior fragments. The genus-zero planar partition producer is proved, not a hypothesis.

   theorem uniform_small_interior_partition (eta : ℝ) (heta : 0 < eta) :
       ∃ K : ℕ, 0 < K ∧
       ∀ (n : ℕ) (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
   …

   Mentions: OAI.HyperbolicObstruction.TableModel.Entry