Commit 2024-07-30 08:33 74f1093c

View on Github →

feat(Combinatorics/SimpleGraph/Connectivity): getVert lemmas (#14977) Add some lemmas about SimpleGraph.Walk.getVert. In preparation for Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

added theorem SimpleGraph.Walk.toSubgraph_adj_getVert

added theorem SimpleGraph.Walk.toSubgraph_adj_iff

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.cons_getVert

added theorem SimpleGraph.Walk.cons_getVert_succ

added theorem SimpleGraph.Walk.cons_sndOfNotNil

added theorem SimpleGraph.Walk.getVert_one

added theorem SimpleGraph.Walk.getVert_tail

added theorem SimpleGraph.Walk.mem_support_iff_exists_getVert

added theorem SimpleGraph.Walk.notNilRec_cons

added theorem SimpleGraph.Walk.tail_cons

added theorem SimpleGraph.Walk.tail_support_eq_support_tail