English
Any equivalence relation on J that contains all morphisms must relate all pairs of objects in a connected category.
Русский
Любое эквивалентное отношение на J, содержащее все морфизмы, должны связывать все пары объектов в связной категории.
LaTeX
$$$[IsPreconnected\ J] \Rightarrow (\forall r: J \to J \to \mathrm{Prop}),\ Equivalence\ r \Rightarrow (\forall \{j_1 j_2 : J\}, (\forall f: j_1 \to j_2, r\ j_1 j_2)) \Rightarrow \forall j_1 j_2 : J, r j_1 j_2$$$
Lean4
/-- Any equivalence relation containing (⟶) holds for all pairs of a connected category. -/
theorem equiv_relation [IsPreconnected J] (r : J → J → Prop) (hr : _root_.Equivalence r)
(h : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), r j₁ j₂) : ∀ j₁ j₂ : J, r j₁ j₂ :=
by
intro j₁ j₂
have z : ∀ j : J, r j₁ j :=
induct_on_objects {k | r j₁ k} (hr.1 j₁) fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
exact z j₂
