Commit 2022-07-11 16:51 0f56b2df

View on Github →

feat(combinatorics/simple_graph/connectivity): simp confluence (#15153) From branch walks_and_trees. Adds data/list/basic lemma to help simp prove d ∈ p.reverse.darts ↔ d.symm ∈ p.darts.

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

modified theorem simple_graph.walk.dart_snd_mem_support_of_mem_darts

added theorem simple_graph.walk.fst_mem_support_of_mem_edges

added theorem simple_graph.walk.is_cycle.not_of_nil

added theorem simple_graph.walk.mem_darts_reverse

deleted theorem simple_graph.walk.mem_support_of_mem_edges

added theorem simple_graph.walk.snd_mem_support_of_mem_edges

Modified src/data/list/basic.lean

added theorem function.involutive.exists_mem_and_apply_eq_iff

added theorem list.mem_map_of_involutive