Commit 2024-07-27 14:22 933a4976

View on Github →

feat(Combinatorics/SimpleGraph): define edist and rewrite dist (#14582) Define edist as the extended distance between two vertices of a simple graph, belonging to ENat, and rewrite dist as the coercion of edist to Nat using toNat. Rewrite the API to meet these new definitions.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.Walk.reverse_bijective

added theorem SimpleGraph.Walk.reverse_injective

added theorem SimpleGraph.Walk.reverse_surjective

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

modified theorem SimpleGraph.Reachable.exists_path_of_dist

modified theorem SimpleGraph.Reachable.of_dist_ne_zero

modified theorem SimpleGraph.Walk.isPath_of_length_eq_dist

modified theorem SimpleGraph.dist_comm

modified theorem SimpleGraph.dist_eq_one_iff_adj

added theorem SimpleGraph.dist_eq_sInf

modified theorem SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable

modified theorem SimpleGraph.dist_eq_zero_of_not_reachable

modified theorem SimpleGraph.dist_le

modified theorem SimpleGraph.dist_ne_zero_iff_ne_and_reachable

modified theorem SimpleGraph.dist_self

added theorem SimpleGraph.edist_comm

added theorem SimpleGraph.edist_eq_one_iff_adj

added theorem SimpleGraph.edist_eq_sInf

added theorem SimpleGraph.edist_eq_top_of_not_reachable

added theorem SimpleGraph.edist_eq_zero_iff

added theorem SimpleGraph.edist_le

added theorem SimpleGraph.edist_ne_top_iff_reachable

added theorem SimpleGraph.edist_pos_of_ne

added theorem SimpleGraph.edist_self

modified theorem SimpleGraph.exists_walk_of_dist_ne_zero

added theorem SimpleGraph.exists_walk_of_edist_eq_coe

added theorem SimpleGraph.exists_walk_of_edist_ne_top

modified theorem SimpleGraph.nonempty_of_pos_dist

added theorem SimpleGraph.reachable_of_edist_ne_top

Modified Mathlib/Data/ENat/Lattice.lean

added theorem ENat.iInf_eq_top_of_isEmpty

added theorem ENat.iInf_eq_zero

added theorem ENat.iInf_toNat