English
If any two objects in a nonempty category J can be linked by a sequence of (possibly reversed) morphisms (a zigzag), then J is connected. This is the converse of exists_zigzag'.
Русский
Если любые две фигуры в ненулевой категории J могут быть связанны последовательностью морфизмов (возможно обратных), то J связна. Это противоположная часть к существованию zigzag'.
LaTeX
$$$ [Nonempty(J)] \\Rightarrow ( \\forall j_1, j_2 : J, \\exists l, List.IsChain(Zag, (j_1 :: l)) \\land List.getLast (j_1 :: l) (List.cons_ne_nil _ _) = j_2 ) \\\\Rightarrow \\\\ IsConnected(J) $$
Lean4
/-- If any two objects in a nonempty category are linked by a sequence of (potentially reversed)
morphisms, then J is connected.
The converse of `exists_zigzag'`.
-/
theorem isConnected_of_zigzag [Nonempty J]
(h : ∀ j₁ j₂ : J, ∃ l, List.IsChain Zag (j₁ :: l) ∧ List.getLast (j₁ :: l) (List.cons_ne_nil _ _) = j₂) :
IsConnected J :=
{ isPreconnected_of_zigzag h with }
