OAI/Analysis/LipschitzHilbert/Geometry/SourceSelectionBoxGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial part of the selected-tree packing argument. Boxes are compared in a common direction before passing to the selecting top's coordinates.

  1. theorem OAI.LipschitzHilbert.common_direction_center_bounds line 11
  2. theorem OAI.LipschitzHilbert.center_in_enlarged_selecting_top line 28