OAI/Geometry/RCD/Coordinates/NormalizedSubplanData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized subplan with its common compression and support

  1. theorem OAI.RegularPointCoordinates.normalized_subplan_data line 15