Commit 2023-03-02 07:55 c97ad7df

View on Github →

feat: Port Combinatorics.SimpleGraph.Metric (#2572)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Metric.lean

added theorem SimpleGraph.dist_comm

added theorem SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable

added theorem SimpleGraph.dist_eq_zero_of_not_reachable

added theorem SimpleGraph.dist_le

added theorem SimpleGraph.dist_self

added theorem SimpleGraph.nonempty_of_pos_dist