English
IsLink e x y is equivalent to Inc e x and Inc e y and all z with Inc e z are either z = x or z = y.
Русский
IsLink e x y эквивалентно Inc e x и Inc e y и для любого z с Inc e z верно z = x или z = y.
LaTeX
$$$G.IsLink e x y \\iff G.Inc e x \\land (G.Inc e y \\land \\forall z, G.Inc e z \\rightarrow z = x \\lor z = y).$$$
Lean4
/-- The binary incidence predicate can be expressed in terms of the unary one. -/
theorem isLink_iff_inc : G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ z, G.Inc e z → z = x ∨ z = y :=
by
refine ⟨fun h ↦ ⟨h.inc_left, h.inc_right, fun z h' ↦ h'.eq_or_eq_of_isLink h⟩, ?_⟩
rintro ⟨⟨x', hx'⟩, ⟨y', hy'⟩, h⟩
obtain rfl | rfl := h _ hx'.inc_right
· obtain rfl | rfl := hx'.left_eq_or_eq hy'
· assumption
exact hy'.symm
assumption
