English
If for every pair j1, j2 we have Zigzag j1 j2, then J is IsPreconnected.
Русский
Если для любых пар j1, j2 выполняется Zigzag j1 j2, то J является IsPreconnected.
LaTeX
$$$\forall J \,[IsPreconnected J]$ или эквивалентно: $(\forall j_1 j_2: J, Zigzag\ j_1 j_2) \Rightarrow IsPreconnected J$$$
Lean4
theorem zigzag_isPreconnected (h : ∀ j₁ j₂ : J, Zigzag j₁ j₂) : IsPreconnected J :=
by
apply IsPreconnected.of_constant_of_preserves_morphisms
intro α F hF j j'
specialize h j j'
induction h with
| refl => rfl
| tail _ hj ih =>
rw [ih]
rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
exacts [hF hj, (hF hj).symm]