Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 22:53 352ecfe1

View on Github →

feat(combinatorics/simple_graph/{connectivity,metric}): connected and dist (#12574)

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added theorem simple_graph.connected.set_univ_walk_nonempty

added structure simple_graph.connected

added theorem simple_graph.preconnected.set_univ_walk_nonempty

added def simple_graph.preconnected

added def simple_graph.reachable

added theorem simple_graph.reachable_iff_nonempty_univ

added theorem simple_graph.reachable_iff_refl_trans_gen

added theorem simple_graph.reachable_is_equivalence

added def simple_graph.reachable_setoid

added def simple_graph.subgraph.connected

added theorem simple_graph.walk.eq_of_length_eq_zero

added theorem simple_graph.walk.exists_length_eq_zero_iff

modified structure simple_graph.walk.is_cycle

modified theorem simple_graph.walk.is_cycle_def

Created src/combinatorics/simple_graph/metric.lean

added theorem simple_graph.connected.dist_eq_zero_iff

added theorem simple_graph.connected.dist_triangle

added theorem simple_graph.connected.exists_walk_of_dist

added theorem simple_graph.connected.pos_dist_of_ne

added def simple_graph.dist

added theorem simple_graph.dist_comm

added theorem simple_graph.dist_comm_aux

added theorem simple_graph.dist_eq_zero_iff_eq_or_not_reachable

added theorem simple_graph.dist_eq_zero_of_not_reachable

added theorem simple_graph.dist_le

added theorem simple_graph.dist_self

added theorem simple_graph.nonempty_of_pos_dist

added theorem simple_graph.reachable.dist_eq_zero_iff

added theorem simple_graph.reachable.exists_walk_of_dist

added theorem simple_graph.reachable.pos_dist_of_ne