OAI/Analysis/CircleDomains/Selection/ProtrusionTestAvailability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local real/mean alternative gives an actual compatible open test at every protruding marked component. All exclusion data are constructed.

  1. theorem OAI.CircleDomainRigidity.exists_protrusion_exclusion_test line 18