OAI/Analysis/CircleDomains/Selection/OrderedProtrusionAvailability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local construction is available against the whole preceding ordered family. Its auxiliary anchor and level code are removed from the returned test, preserving the original physical data and open exclusion.

  1. theorem OAI.CircleDomainRigidity.exists_ordered_protrusion_test line 21