OAI/Analysis/CircleDomains/Selection/DelayedSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reserve the first coordinate slot for the zero test while preserving all selected tests and their order.

  1. def OAI.CircleDomainRigidity.delayedSelection line 12
  2. theorem OAI.CircleDomainRigidity.delayedSelection_mono line 16
  3. theorem OAI.CircleDomainRigidity.delayedSelection_single line 24
  4. theorem OAI.CircleDomainRigidity.iUnion_delayedSelection line 31