edist_eq_one_iff_adj — Mathlib

English

edist u v = 1 iff u and v are adjacent.

Русский

edist u v = 1 тогда и только тогда, когда u и v смежны.

LaTeX

$$$ G.edist u v = 1 \iff G.Adj u v $$$

Lean4

/-- The extended distance between vertices is equal to `1` if and only if these vertices are adjacent.
-/
@[simp]
theorem edist_eq_one_iff_adj : G.edist u v = 1 ↔ G.Adj u v :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp
    exact w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw
  · exact le_antisymm (edist_le h.toWalk) (Order.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)

Похожие утверждения