OAI/Analysis/LipschitzHilbert/Geometry/PopularGroupDirections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Directions in one overlapping projected-popularity group are close. This uses actual popularity points with the same long coordinate.

  1. theorem OAI.LipschitzHilbert.Rectangle.popular_group_directions line 12