English
Same inductive principle for objects as before: if p is nonempty and closed under morphisms, then every object belongs to p.
Русский
Та же индуктивная формула для объектов: если p непусто и замкнуто по морфизмам, то каждый объект лежит в p.
LaTeX
$$$\\operatorname{IsPreconnected}(J) \\Rightarrow \\forall p \\subset J,\\ p\\neq \\varnothing \\to (\\forall \\{j_1,j_2\\} (f: j_1\\to j_2), j_1\\in p \\iff j_2\\in p) \\to \\forall j:\\,J, j\\in p$$$
Lean4
/-- An inductive-like property for the objects of a connected category.
If the set `p` is nonempty, and `p` is closed under morphisms of `J`,
then `p` contains all of `J`.
The converse is given in `IsConnected.of_induct`.
-/
theorem induct_on_objects [IsPreconnected J] (p : Set J) {j₀ : J} (h0 : j₀ ∈ p)
(h1 : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) (j : J) : j ∈ p :=
by
let aux (j₁ j₂ : J) (f : j₁ ⟶ j₂) := congrArg ULift.up <| (h1 f).eq
injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i
rwa [i]
