OAI/Analysis/CircleDomains/Rigidity/MaskAtlasGeometricAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Assemble physical collision terminals and the remaining filling contours for a mixed finite list. Nonsingular local real branches give terminal bounds; closed level graphs give the filling geometry.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_mask_atlas_geometric_assembly line 18