OAI/Analysis/Conductivity/Sources/WordGeometry.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.sourceChildEuclidean_eq_similarity line 12
  2. lemma OAI.ScalarConductivity.source_child_closed_subset line 17
  3. lemma OAI.ScalarConductivity.source_child_closed_disjoint line 24
  4. abbrev OAI.ScalarConductivity.SourceWord line 34
  5. def OAI.ScalarConductivity.sourceWordMap line 36
  6. lemma OAI.ScalarConductivity.sourceWordMap_nil line 40
  7. lemma OAI.ScalarConductivity.sourceWordMap_cons line 41
  8. lemma OAI.ScalarConductivity.sourceWordMap_append line 44
  9. lemma OAI.ScalarConductivity.sourceWordMap_dist line 50
  10. lemma OAI.ScalarConductivity.sourceWordMap_closed_subset line 58
  11. def OAI.ScalarConductivity.sourceWordCell line 67
  12. def OAI.ScalarConductivity.sourceWordBlock line 69
  13. lemma OAI.ScalarConductivity.sourceWordCell_subset line 71
  14. lemma OAI.ScalarConductivity.sourceWordBlock_subset_cell line 73
  15. lemma OAI.ScalarConductivity.sourceWordBlock_isOpen line 76
  16. lemma OAI.ScalarConductivity.sourceWordCell_isCompact line 79
  17. lemma OAI.ScalarConductivity.sourceWordCell_cons_subset line 82
  18. lemma OAI.ScalarConductivity.sourceWordBlock_cons line 87
  19. lemma OAI.ScalarConductivity.sourceWordBlock_nil_cons_disjoint line 93
  20. lemma OAI.ScalarConductivity.sourceWordBlock_disjoint line 106
  21. lemma OAI.ScalarConductivity.sourceWordBlock_unique line 130
  22. lemma OAI.ScalarConductivity.sourceWordBlock_root line 135
  23. lemma OAI.ScalarConductivity.sourceWordBlock_child_iff line 139