edist_comm — Mathlib

English

The extended distance is symmetric: edist u v = edist v u.

Русский

Расстояние в расширенном смысле симметрично: edist u v = edist v u.

LaTeX

$$$ G.edist u v = G.edist v u $$$

Lean4

theorem edist_comm : G.edist u v = G.edist v u :=
  by
  rw [edist_eq_sInf, ← Set.image_univ, ← Set.image_univ_of_surjective Walk.reverse_surjective, ← Set.image_comp,
    Set.image_univ, Function.comp_def]
  simp_rw [Walk.length_reverse, ← edist_eq_sInf]

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