Commit 2025-02-19 07:30 2ee17ff1

View on Github →

feat(Combinatorics/SimpleGraphs): various path and edge lemmas (#22034) Adds a number of miscellaneous lemmas, mostly on paths and edges, in preparation for Tutte's theorem.

Estimated changes

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

added theorem SimpleGraph.Walk.IsCycle.exists_isCycle_snd_verts_eq

added theorem SimpleGraph.Walk.adj_toSubgraph_mapLe

added theorem SimpleGraph.Walk.not_nil_of_adj_toSubgraph

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Hom.mapSpanningSubgraphs_inj

added theorem SimpleGraph.Hom.mapSpanningSubgraphs_injective

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.IsAlternating.spanningCoe

added theorem SimpleGraph.IsAlternating.sup_edge

added theorem SimpleGraph.Subgraph.IsMatching.not_adj_left_of_ne

added theorem SimpleGraph.Subgraph.IsMatching.not_adj_right_of_ne

added theorem SimpleGraph.Walk.IsCycle.adj_toSubgraph_iff_of_isCycles

added theorem SimpleGraph.Walk.IsCycle.isCycles_spanningCoe_toSubgraph

added theorem SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

added theorem SimpleGraph.adj_edge

added theorem SimpleGraph.disjoint_edge

added theorem SimpleGraph.sdiff_edge

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Walk.IsPath.getVert_eq_end_iff

added theorem SimpleGraph.Walk.IsPath.getVert_eq_start_iff

added theorem SimpleGraph.Walk.IsPath.getVert_injOn_iff