OAI/Analysis/CircleDomains/Modulus/RealBarrierTests.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual real tests used by the countable selection. Compatibility is with every finite sublist of previously selected tests, retaining repetitions.

  1. structure OAI.CircleDomainRigidity.UngatedRealTest line 19
  2. def OAI.CircleDomainRigidity.UngatedRealTest.size line 38
  3. theorem OAI.CircleDomainRigidity.UngatedRealTest.ordinary_norm_le_size line 43
  4. def OAI.CircleDomainRigidity.UngatedRealTest.openEnds line 68
  5. theorem OAI.CircleDomainRigidity.UngatedRealTest.open_openEnds line 70
  6. def OAI.CircleDomainRigidity.UngatedRealTest.CompatibleWith line 73
  7. theorem OAI.CircleDomainRigidity.UngatedRealTest.CompatibleWith.mono line 82
  8. def OAI.CircleDomainRigidity.UngatedRealTest.of_barrier line 87
  9. theorem OAI.CircleDomainRigidity.UngatedRealTest.size_of_barrier line 103
  10. theorem OAI.CircleDomainRigidity.UngatedRealTest.freeComponentFailure_congr_selected line 110
  11. theorem OAI.CircleDomainRigidity.UngatedRealTest.of_barrier_compatible line 123