edist_pos_of_ne

Mathlib.Combinatorics.SimpleGraph.Metric

URI: https://scilib.ai/kg/mathlib#SimpleGraph.edist_pos_of_ne

English

If u ≠ v, then edist u v > 0.

Русский

Если u не равно v, то edist u v > 0.

LaTeX

$$$ u \neq v \Rightarrow 0 < G.edist u v $$$

Lean4

theorem edist_pos_of_ne (hne : u ≠ v) : 0 < G.edist u v :=
  pos_iff_ne_zero.mpr <| edist_eq_zero_iff.ne.mpr hne

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru