of_constant_of_preserves_morphisms

English

If J and K are equivalent, then if J is preconnected, K is as well.

Русский

Если J и K эквивалентны, то предсвязность J переносится на K.

LaTeX

$$$\\text{If } e:\\,J \\simeq K,\\text{ then } IsPreconnected(J) \\Rightarrow IsPreconnected(K).$$$

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 [Nonempty J]
    (h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ j j' : J, F j = F j') :
    IsConnected J :=
  { IsPreconnected.of_constant_of_preserves_morphisms h with }

Похожие утверждения