left_eq_of_right_ne

Mathlib.Combinatorics.Graph.Basic

URI: https://scilib.ai/kg/mathlib#Graph.IsLink.left_eq_of_right_ne

English

If h: G.IsLink e x y and h': G.IsLink e z w and x ≠ z, then x = w.

Русский

Если h: IsLink e x y и h': IsLink e z w и x ≠ z, то x = w.

LaTeX

$$$\\text{If } G.IsLink\\,e\\,x\\,y \\text{ and } G.IsLink\\,e\\,z\\,w \\text{ and } x \\neq z, \\text{ then } x = w.$$$

Lean4

theorem left_eq_of_right_ne (h : G.IsLink e x y) (h' : G.IsLink e z w) (hzx : x ≠ z) : x = w :=
  (h.left_eq_or_eq h').elim (False.elim ∘ hzx) id

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

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

Разделы

Аффилиация

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