OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedSupportedGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Assigned reference geometry follows from the centers of the selected packets. No global longest-scale hypothesis is required.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_supportedTopGeometry line 16