Commit 2026-10-17 17:39 acf39817

View on Github →

feat(Combinatorics/SimpleGraph/Metric): add distance lemmas for graph maps (#44872) Graph homomorphisms map walks to walks of the same length, so they do not increase extended graph distance. For natural-valued distance, the corresponding bound requires source reachability because unreachable pairs use the junk value 0. Add:

  • SimpleGraph.Hom.edist_le
  • SimpleGraph.Iso.edist_eq
  • SimpleGraph.Hom.dist_le
  • SimpleGraph.Iso.dist_eq Mark both isomorphism equalities as @[simp]. Refactor the existing distance-antitonicity results for graph inclusions through Hom.ofLE, making them special cases of the homomorphism bounds. Discussed on Zulip: distance and balls under graph maps.

Estimated changes