OAI/Topology/ArtinGroups/Harmonic/Crossing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.GraphConnection.crossing line 10
2. def OAI.HarmonicArtin.GraphConnection.neighbors line 15
3. lemma OAI.HarmonicArtin.GraphConnection.mem_neighbors line 18
4. theorem OAI.HarmonicArtin.GraphConnection.crossing_square line 21
5. lemma OAI.HarmonicArtin.GraphConnection.exists_crossing_parameter line 88
6. def OAI.HarmonicArtin.GraphConnection.cupCap line 109
7. lemma OAI.HarmonicArtin.GraphConnection.cupCap_square line 113
8. lemma OAI.HarmonicArtin.GraphConnection.crossing_matrix_inverse line 128