eq_or_eq_or_eq — Mathlib

English

Let G be a graph and e an edge that is incident to vertices x, y, and z. Then at least two of x, y, z are equal.

Русский

Пусть G — граф и e — ребро, инцидентное вершинам x, y и z. Тогда две из x, y и z совпадают.

LaTeX

$$$G.Inc\\ e\\ x\\land G.Inc\\ e\\ y\\land G.Inc\\ e\\ z\\Rightarrow x= y\\lor x= z\\lor y= z$$$

Lean4

theorem eq_or_eq_or_eq (hx : G.Inc e x) (hy : G.Inc e y) (hz : G.Inc e z) : x = y ∨ x = z ∨ y = z :=
  by
  by_contra! hcon
  obtain ⟨x', hx'⟩ := hx
  obtain rfl := hy.eq_of_isLink_of_ne_left hx' hcon.1.symm
  obtain rfl := hz.eq_of_isLink_of_ne_left hx' hcon.2.1.symm
  exact hcon.2.2 rfl

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