OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedSupportedGeometry.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.SourceLabeledLattice.assignedTopReference_supportedTopGeometry line 16