Commit 2026-06-01 01:24 62e42dba
View on Github →feat(Combinatorics/SimpleGraph/Walk): upgrade subset theorems to sublist/prefix/suffix (#37577)
Upgrades theorems about p.support ⊆ q.support / p.darts ⊆ q.darts / p.edges ⊆ q.edges to List.IsInfix/List.IsSuffix/List.Sublist, which imply the subset versions.
Also adds cycleBypass sublist lemmas that were missing, and golfs length_bypass_le and bypass_eq_self_of_length_le using the new sublist theorems.