English
If any maximal connected component containing j0 is all of J, then J is connected.
Русский
Если любая максимальная связная компонента, содержащая j0, есть вся J, то J связно.
LaTeX
$$$\\text{If } h:\\forall p\\subset J, j_0\\in p\\to (\\forall {j_1 j_2}, (f: j_1\\to j_2)\\to (j_1\\in p \\iff j_2\\in p))\\to \\forall j:\\,J, j\\in p \\Rightarrow \\ IsConnected(J).$$$
Lean4
/-- If any maximal connected component containing some element j₀ of J is all of J, then J is connected.
The converse of `induct_on_objects`.
-/
theorem of_induct {j₀ : J} (h : ∀ p : Set J, j₀ ∈ p → (∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ j : J, j ∈ p) :
IsConnected J :=
have := Nonempty.intro j₀
IsConnected.of_constant_of_preserves_morphisms fun {α} F a =>
by
have w :=
h {j | F j = F j₀} rfl
(fun {j₁} {j₂} f => by
change F j₁ = F j₀ ↔ F j₂ = F j₀
simp [a f])
intro j j'
rw [w j, w j']
