OAI/Analysis/Conductivity/Branching/JoinHull.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.joinHull line 22
  2. lemma OAI.ScalarConductivity.subset_joinHull line 26
  3. lemma OAI.ScalarConductivity.joinHull_mono line 28
  4. lemma OAI.ScalarConductivity.joinHull_subset_laminate line 33
  5. lemma OAI.ScalarConductivity.isOpen_joinHull line 40
  6. lemma OAI.ScalarConductivity.joinHull_permute line 60
  7. def OAI.ScalarConductivity.depthClass line 72
  8. lemma OAI.ScalarConductivity.depthClass_subset_succ line 76
  9. lemma OAI.ScalarConductivity.depthClass_mono line 79
  10. lemma OAI.ScalarConductivity.depthClass_subset_laminate line 82
  11. lemma OAI.ScalarConductivity.isOpen_depthClass line 89
  12. lemma OAI.ScalarConductivity.depthClass_permute line 96
  13. theorem OAI.ScalarConductivity.IsFiniteLaminate.mem_some_depth line 103
  14. theorem OAI.ScalarConductivity.depthClass_plan line 116
  15. def OAI.ScalarConductivity.scalarNeighbourhood line 138
  16. lemma OAI.ScalarConductivity.isOpen_scalarNeighbourhood line 141
  17. lemma OAI.ScalarConductivity.scalar_mem_scalarNeighbourhood line 150
  18. lemma OAI.ScalarConductivity.scalarNeighbourhood_permute line 155
  19. def OAI.ScalarConductivity.endpointGraph line 171
  20. lemma OAI.ScalarConductivity.isOpen_endpointGraph line 174
  21. lemma OAI.ScalarConductivity.path_mem_endpointGraph line 184