Commit 2023-02-16 14:01 13cd3e89

View on Github →

feat(combinatorics/simple_graph/connectivity): concat and concat_rec (#17209) Adds the alternative constructor for walks along with its recursion principle. (Borrowed from lean2/hott.)

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added theorem simple_graph.walk.append_concat

added def simple_graph.walk.concat

added theorem simple_graph.walk.concat_append

added theorem simple_graph.walk.concat_cons

added theorem simple_graph.walk.concat_eq_append

added theorem simple_graph.walk.concat_inj

added theorem simple_graph.walk.concat_ne_nil

added theorem simple_graph.walk.concat_nil

added def simple_graph.walk.concat_rec

added def simple_graph.walk.concat_rec_aux

added theorem simple_graph.walk.concat_rec_concat

added theorem simple_graph.walk.concat_rec_nil

added theorem simple_graph.walk.darts_concat

added theorem simple_graph.walk.edges_concat

added theorem simple_graph.walk.exists_concat_eq_cons

added theorem simple_graph.walk.exists_cons_eq_concat

added theorem simple_graph.walk.length_concat

added theorem simple_graph.walk.reverse_concat

added theorem simple_graph.walk.support_concat

Modified src/logic/basic.lean

added theorem heq_rec_iff_heq

added theorem rec_heq_iff_heq

modified theorem rec_heq_of_heq