OAI/Combinatorics/ThinTrees/MatrixDomain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.isClosed_psd line 15
  2. lemma OAI.StrongThinTree.isClosed_matrixAbove line 27
  3. lemma OAI.StrongThinTree.psd_entry_bound line 29
  4. def OAI.StrongThinTree.MultiGraph.matrixDomain line 42
  5. lemma OAI.StrongThinTree.MultiGraph.domain_pd line 45
  6. lemma OAI.StrongThinTree.MultiGraph.domain_closed line 47
  7. lemma OAI.StrongThinTree.MultiGraph.domain_convex line 51
  8. lemma OAI.StrongThinTree.MultiGraph.domain_nonempty line 61
  9. lemma OAI.StrongThinTree.MultiGraph.indicator_singleton line 69
  10. lemma OAI.StrongThinTree.MultiGraph.domain_diag_bound line 72
  11. lemma OAI.StrongThinTree.MultiGraph.domain_bounded line 83
  12. lemma OAI.StrongThinTree.MultiGraph.domain_compact line 93
  13. lemma OAI.StrongThinTree.MultiGraph.resistance_continuousAt line 95
  14. lemma OAI.StrongThinTree.MultiGraph.resistance_continuousOn line 100