English
IsChain R (a :: l) holds iff l = [] or there exists b, l' with R a b and IsChain R (b :: l') and l = b :: l'.
Русский
IsChain R (a :: l) эквивалентно (l = []) или существует b, l' такие, что R a b и IsChain R (b :: l') и l = b :: l'.
LaTeX
$$$IsChain\\;R\\;(a :: l) \\iff l = [] \\lor \\exists b\\; \\exists l'\\; (R\\,a\\,b) \\land IsChain\\;R\\;(b :: l') \\land l = b :: l'$$$
Lean4
theorem isChain_cons_iff (R : α → α → Prop) (a : α) (l : List α) :
IsChain R (a :: l) ↔ l = [] ∨ ∃ (b : α) (l' : List α), R a b ∧ IsChain R (b :: l') ∧ l = b :: l' :=
(isChain_iff _ _).trans <|
by
simp only [cons_ne_nil, List.cons_eq_cons, exists_and_right, exists_eq', true_and, exists_and_left, false_or]
grind
