English
If J is connected, then for any objects j1, j2 in J there exists a finite zigzag from j1 to j2, i.e., a list l such that j1 :: l forms a zigzag chain ending at j2.
Русский
Если J связна, то для любых объектов j1, j2 в J существует конечная зигзагообразная цепь от j1 к j2, то есть существует список l так, что j1 :: l образует зигзагообразную цепь, получающуюся в конце j2.
LaTeX
$$$ [IsConnected(J)] \\Rightarrow \\exists l, List.IsChain(Zag, (j_1 :: l)) \\land List.getLast(j_1 :: l) (List.cons_ne_nil _) = j_2$$
Lean4
theorem exists_zigzag' [IsConnected J] (j₁ j₂ : J) :
∃ l, List.IsChain Zag (j₁ :: l) ∧ List.getLast (j₁ :: l) (List.cons_ne_nil _ _) = j₂ :=
List.exists_isChain_cons_of_relationReflTransGen (isPreconnected_zigzag _ _)
