eq_and_eq_or_eq_and_eq — Mathlib

English

If G.IsLink e x y and G.IsLink e x' y', then either x = x' and y = y', or x = y' and y = x'.

Русский

Если IsLink e x y и IsLink e x' y', то либо x = x' и y = y', либо x = y' и y = x'.

LaTeX

$$$G.IsLink\\,e\\,x\\,y \\rightarrow G.IsLink\\,e\\,x'\\,y' \\Rightarrow (x = x' \\land y = y') \\lor (x = y' \\land y = x').$$$

Lean4

theorem eq_and_eq_or_eq_and_eq {x' y' : α} (h : G.IsLink e x y) (h' : G.IsLink e x' y') :
    (x = x' ∧ y = y') ∨ (x = y' ∧ y = x') :=
  by
  obtain rfl | rfl := h.left_eq_or_eq h'
  · simp [h.right_unique h']
  simp [h'.symm.right_unique h]

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