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[].

Estimated changes