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