Commit 2025-06-20 23:24 2e2176e9
View on Github →feat(SimpleGraph): Small refactor + helper lemma (#25654)
There exists a Walk.getVert_eq_support_get?
lemma to relate Walk.getVert
and Walk.support[]?
. Small refactor: this should be named _getElem?
instead of _get?
.
Further, I add another lemma that relates getVert
to support[]
(without the ?
) and then derive the getElem?
theorem from it, to simplify cases when you are working with support[]
.