OAI/Analysis/Conductivity/Branching/CentralJoinCover.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.centralPhysical_subset_ball line 11
  2. lemma OAI.ScalarConductivity.centralPhysical_mem_interior_of_strict line 25
  3. def OAI.ScalarConductivity.centralJoinOpen line 38
  4. lemma OAI.ScalarConductivity.centralJoinOpen_isOpen line 44
  5. lemma OAI.ScalarConductivity.centralJoinOpen_covers line 52
  6. theorem OAI.ScalarConductivity.exists_centralJoinPartition line 78
  7. theorem OAI.ScalarConductivity.exists_centralJoinPartition_neighborhood line 84
  8. def OAI.ScalarConductivity.centralJoinPartition line 104
  9. lemma OAI.ScalarConductivity.centralJoinPartition_subordinate line 108
  10. lemma OAI.ScalarConductivity.centralJoinPartition_eventually_sum line 111
  11. lemma OAI.ScalarConductivity.centralJoinPartition_smooth line 115
  12. lemma OAI.ScalarConductivity.centralJoinPartition_bound line 118
  13. lemma OAI.ScalarConductivity.centralJoinPartition_interior_support line 122
  14. lemma OAI.ScalarConductivity.centralJoinPartition_interior_compact line 125
  15. lemma OAI.ScalarConductivity.centralJoinPartition_parent_support line 128
  16. lemma OAI.ScalarConductivity.centralJoinPartition_parent_compact line 135
  17. def OAI.ScalarConductivity.centralChildPatch line 139
  18. def OAI.ScalarConductivity.centralJoinChildCutoff line 141
  19. lemma OAI.ScalarConductivity.centralJoinChildCutoff_smooth line 144
  20. lemma OAI.ScalarConductivity.centralJoinChildCutoff_bound line 148
  21. lemma OAI.ScalarConductivity.centralJoinChildCutoff_support line 151
  22. lemma OAI.ScalarConductivity.centralJoinChildCutoff_compact line 167
  23. lemma OAI.ScalarConductivity.centralJoinPartition_sum line 171
  24. lemma OAI.ScalarConductivity.centralJoinPartition_derivative_sum line 175