Commit 2025-09-15 16:49 ea49cde8
View on Github →feat(SimpleGraph/Walk): add missing results involving getVert / takeUntil (#29601)
Add some missing lemmas involving getVert / takeUntil.
In particular getVert_le_length_takeUntil_eq_iff which says that if p is a walk containing the vertex u then n = (p.takeUntil u h).length is the smallest n such that p.getVert n = u.