English
If for every pair of objects j1, j2 there exists a zigzag chain from j1 to j2 (as in the previous lemma), then J is preconnected. This is the forward direction of the equivalence with exists_zigzag'.
Русский
Если для любых объектов j1, j2 сущестует зигзак-цепь от j1 к j2, то J является предсвязанной. Это направление к эквивалентности с существованием zigzag'.
LaTeX
$$$ \\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 \\\\ IsPreconnected(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 isPreconnected_of_zigzag
(h : ∀ j₁ j₂ : J, ∃ l, List.IsChain Zag (j₁ :: l) ∧ List.getLast (j₁ :: l) (List.cons_ne_nil _ _) = j₂) :
IsPreconnected J := by
apply zigzag_isPreconnected
intro j₁ j₂
rcases h j₁ j₂ with ⟨l, hl₁, hl₂⟩
apply List.relationReflTransGen_of_exists_isChain_cons l hl₁ hl₂
