isPreconnected_zigzag — Mathlib

English

In a category that is preconnected, any two objects are related by Zigzag.

Русский

В предсвязной категории любые два объекта связаны Zigzag.

LaTeX

$$$[IsPreconnected\ J] \Rightarrow \forall j_1 j_2: J,\ Zigzag\ j_1 j_2$$$

Lean4

/-- In a connected category, any two objects are related by `Zigzag`. -/
theorem isPreconnected_zigzag [IsPreconnected J] (j₁ j₂ : J) : Zigzag j₁ j₂ :=
  equiv_relation _ zigzag_equivalence (fun f => Relation.ReflTransGen.single (Or.inl (Nonempty.intro f))) _ _

Похожие утверждения