Commit 2021-12-27 16:46 ae8f08fe

View on Github →

feat(combinatorics/simple_graph/connectivity): more lemmas (#11010) This is the second chunk of #8737, which gives some more lemmas for manipulating the support and edge lists of walks. This also turns is_trail back into a structure.

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added theorem simple_graph.walk.coe_support

added theorem simple_graph.walk.coe_support_append'

added theorem simple_graph.walk.coe_support_append

deleted theorem simple_graph.walk.count_edges_eq_one_of_trail

deleted theorem simple_graph.walk.count_edges_le_one_of_trail

added theorem simple_graph.walk.edges_append

added theorem simple_graph.walk.edges_nodup_of_support_nodup

added theorem simple_graph.walk.edges_reverse

added theorem simple_graph.walk.end_mem_tail_support_of_ne

added theorem simple_graph.walk.exists_eq_cons_of_ne

modified structure simple_graph.walk.is_circuit

modified structure simple_graph.walk.is_cycle

added theorem simple_graph.walk.is_path.mk'

added theorem simple_graph.walk.is_path.nil

added theorem simple_graph.walk.is_path.of_append_left

added theorem simple_graph.walk.is_path.of_append_right

added theorem simple_graph.walk.is_path.of_cons

added theorem simple_graph.walk.is_path.reverse

modified structure simple_graph.walk.is_path

modified theorem simple_graph.walk.is_path_def

deleted theorem simple_graph.walk.is_path_of_cons_is_path

added theorem simple_graph.walk.is_path_reverse_iff

added theorem simple_graph.walk.is_trail.count_edges_eq_one

added theorem simple_graph.walk.is_trail.count_edges_le_one

added theorem simple_graph.walk.is_trail.nil

added theorem simple_graph.walk.is_trail.of_append_left

added theorem simple_graph.walk.is_trail.of_append_right

added theorem simple_graph.walk.is_trail.of_cons

added theorem simple_graph.walk.is_trail.reverse

added structure simple_graph.walk.is_trail

deleted def simple_graph.walk.is_trail

added theorem simple_graph.walk.is_trail_def

deleted theorem simple_graph.walk.is_trail_of_cons_is_trail

added theorem simple_graph.walk.mem_support_append_iff

added theorem simple_graph.walk.mem_support_iff

modified theorem simple_graph.walk.mem_support_of_mem_edges

added theorem simple_graph.walk.mem_tail_support_append_iff

deleted theorem simple_graph.walk.nil_is_path

deleted theorem simple_graph.walk.nil_is_trail

added theorem simple_graph.walk.reverse_is_trail_iff

added theorem simple_graph.walk.support_append

deleted theorem simple_graph.walk.support_eq

added theorem simple_graph.walk.support_eq_cons

added theorem simple_graph.walk.support_reverse

added theorem simple_graph.walk.tail_support_append