OAI/Analysis/SegmentLenses/Identifications.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Hilbertian congruences and forest identifications

  1. def OAI.SegmentLenses.l2Congr line 25
  2. theorem OAI.SegmentLenses.l2Congr_apply line 37
  3. def OAI.SegmentLenses.SegmentEmbedding.testEquivOfSurjective line 47
  4. def OAI.SegmentLenses.SegmentEmbedding.primalEquivOfSurjective line 52
  5. theorem OAI.SegmentLenses.SegmentEmbedding.primalEquivOfSurjective_test line 56
  6. abbrev OAI.SegmentLenses.ComponentPartition.BlockVertex line 69
  7. def OAI.SegmentLenses.ComponentPartition.regionEmbedding line 72
  8. theorem OAI.SegmentLenses.ComponentPartition.regionEmbedding_range line 75
  9. def OAI.SegmentLenses.ComponentPartition.regionTestMap line 84
  10. theorem OAI.SegmentLenses.ComponentPartition.regionTestMap_surjective line 100
  11. def OAI.SegmentLenses.ComponentPartition.regionTestEquiv line 110
  12. def OAI.SegmentLenses.ComponentPartition.regionPrimalEquiv line 113
  13. theorem OAI.SegmentLenses.ComponentPartition.regionPrimalEquiv_test line 116
  14. def OAI.SegmentLenses.ComponentPartition.regionL2Equiv line 122
  15. def OAI.SegmentLenses.ComponentPartition.regionDualL2Equiv line 127
  16. def OAI.SegmentLenses.SingleTree.Vertex line 137
  17. instance OAI.SegmentLenses.SingleTree.(instance at line 138) line 138
  18. instance OAI.SegmentLenses.SingleTree.(instance at line 139) line 139
  19. instance OAI.SegmentLenses.SingleTree.(instance at line 140) line 140
  20. instance OAI.SegmentLenses.SingleTree.(instance at line 141) line 141
  21. instance OAI.SegmentLenses.SingleTree.(instance at line 142) line 142
  22. instance OAI.SegmentLenses.SingleTree.(instance at line 143) line 143
  23. instance OAI.SegmentLenses.SingleTree.(instance at line 144) line 144
  24. abbrev OAI.SegmentLenses.SingleTree.J line 148
  25. abbrev OAI.SegmentLenses.SingleTree.X line 149
  26. def OAI.SegmentLenses.SingleTree.componentOrderEmbedding line 154
  27. theorem OAI.SegmentLenses.SingleTree.componentEmbedding_range line 159
  28. def OAI.SegmentLenses.SingleTree.componentEmbedding line 171
  29. theorem OAI.SegmentLenses.SingleTree.componentEmbedding_apply line 178
  30. def OAI.SegmentLenses.SingleTree.componentTestMap line 181
  31. theorem OAI.SegmentLenses.SingleTree.componentTestMap_surjective line 198
  32. def OAI.SegmentLenses.SingleTree.componentTestEquiv line 211
  33. def OAI.SegmentLenses.SingleTree.componentPrimalEquiv line 216
  34. theorem OAI.SegmentLenses.SingleTree.componentPrimalEquiv_test line 219
  35. def OAI.SegmentLenses.IndexedForest.singleTreeL2Equiv line 233
  36. def OAI.SegmentLenses.IndexedForest.singleTreeDualL2Equiv line 238
  37. theorem OAI.SegmentLenses.IndexedForest.singleTreeDualL2Equiv_on_test line 243