English
An inductive-like property: if p ⊆ J is nonempty and closed under morphisms of J, then every object is in p.
Русский
Индуктивная подобная свойство: если p ⊆ J непусто и замкнута по морфизмам, то все объекты принадлежат p.
LaTeX
$$$\\operatorname{IsPreconnected}(J) \\Rightarrow \\forall p \\subset J,\\ j_0 \\in p \\to (\\forall \\{j_1,j_2\\}:J\\,(f: j_1\\to j_2), j_1\\in p \\leftrightarrow j_2\\in p) \\to \\forall j:\\,J, j\\in p$$$
Lean4
/-- `J` is connected if: given any function `F : J → α` which is constant for any
`j₁, j₂` for which there is a morphism `j₁ ⟶ j₂`, then `F` is constant.
This can be thought of as a local-to-global property.
The converse of `constant_of_preserves_morphisms`.
-/
theorem of_constant_of_preserves_morphisms
(h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ j j' : J, F j = F j') :
IsPreconnected J :=
IsPreconnected.of_any_functor_const_on_obj fun F => h F.obj fun f => by ext; exact Discrete.eq_of_hom (F.map f)
