Theorem SimpleGraph.Hom.dist_le

Modification history

2026-10-17 17:39
Mathlib/Combinatorics/SimpleGraph/Metric.lean
feat(Combinatorics/SimpleGraph/Metric): add distance lemmas for graph maps (#44872) …
Added SimpleGraph.Hom.dist_leView on Github →