English
If J is connected, then any function F: J → α with the property F(j1)=F(j2) whenever there is a morphism j1 ⟶ j2 is constant.
Русский
Если J связано, то любая функция F: J → α, которая сохраняет равенство по morphism, постоянна на J.
LaTeX
$$$[\\mathrm{IsPreconnected}(J)] \\Rightarrow \\forall \\alpha, \\forall F: J \\to \\alpha, (\\forall j_1 j_2, j_1 \\to j_2 \\Rightarrow F(j_1)=F(j_2)) \\Rightarrow \\forall j,j': J, F(j)=F(j').$$$
Lean4
/-- If `J` is connected, then given any function `F` such that the presence of a
morphism `j₁ ⟶ j₂` implies `F j₁ = F j₂`, we have that `F` is constant.
This can be thought of as a local-to-global property.
The converse is shown in `IsConnected.of_constant_of_preserves_morphisms`
-/
theorem constant_of_preserves_morphisms [IsPreconnected J] {α : Type u₂} (F : J → α)
(h : ∀ (j₁ j₂ : J) (_ : j₁ ⟶ j₂), F j₁ = F j₂) (j j' : J) : F j = F j' := by
simpa using
any_functor_const_on_obj
{ obj := Discrete.mk ∘ F
map := fun f => eqToHom (by ext; exact h _ _ f) } j j'
