OAI/Geometry/PinnedDistances/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakPinned.mainStatement line 12

   Source documentation

   Uniform weak pinned planar distances for arbitrary real configurations.

   theorem mainStatement : MainStatement := by
   …

   Mentions: OAI.WeakPinned.MainStatement

2. theorem OAI.WeakPinned.main line 29

   Distinct definitions of this name: ComparatorChallenges/PinnedDistances.lean:29 (same statement text; different proof or body). Qualify references as OAI.WeakPinned.main@path.