Commit 2025-01-16 12:28 71e670b6

View on Github →

feat(Combinatorics/SimpleGraph): vertices in cycles (#20602) This adds various lemmas on vertices in cycles: Non-equality, and the exact neighbors and size of the neighborSet, along with some smaller supporting lemmas for walks. In preparation for Tutte's theorem.

Estimated changes

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

added theorem SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two

added theorem SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpoint

added theorem SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_internal

added theorem SimpleGraph.Walk.toSubgraph_adj_penultimate

added theorem SimpleGraph.Walk.toSubgraph_adj_snd

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Walk.IsCycle.getVert_endpoint_iff

added theorem SimpleGraph.Walk.IsCycle.getVert_injOn'

added theorem SimpleGraph.Walk.IsCycle.getVert_injOn

added theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_neq_getVert_add_one

added theorem SimpleGraph.Walk.IsCycle.snd_ne_penultimate

added theorem SimpleGraph.Walk.not_nil_of_isCycle_cons

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.not_nil_of_tail_not_nil