OAI/Probability/SpanningForest/FiniteCycleIncidence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Problem336.finiteCodeEdgesFintype line 11
  2. def OAI.Problem336.finiteFlowEmbedding line 14
  3. theorem OAI.Problem336.finiteFlowEmbedding_apply line 18
  4. theorem OAI.Problem336.finiteFlowEmbedding_range line 31
  5. theorem OAI.Problem336.finiteFlowEmbedding_injective line 38
  6. def OAI.Problem336.finiteIncidence line 44
  7. theorem OAI.Problem336.finiteIncidence_mulVec line 48
  8. theorem OAI.Problem336.IsFiniteConnectedSubgraph.boundary_eq_zero_outside line 61
  9. theorem OAI.Problem336.IsFiniteConnectedSubgraph.finiteCycleSpace_eq_incidenceKernel line 76
  10. theorem OAI.Problem336.IsFiniteConnectedSubgraph.finiteHilbertCycleSpace_eq_incidenceKernel line 105
  11. def OAI.Problem336.finiteHilbertEmbeddingLinear line 112
  12. theorem OAI.Problem336.finiteHilbertEmbeddingLinear_apply line 117
  13. theorem OAI.Problem336.finiteHilbertEmbeddingLinear_sum line 122
  14. theorem OAI.Problem336.finiteHilbertEmbeddingLinear_inner line 129
  15. def OAI.Problem336.finiteHilbertEmbedding line 138
  16. theorem OAI.Problem336.finiteHilbertEmbedding_apply line 142
  17. theorem OAI.Problem336.IsFiniteConnectedSubgraph.finiteHilbertCycleSpace_eq_euclideanKernel line 147