prod — Mathlib

English

If J and K are preconnected, then J × K is preconnected.

Русский

Если J и K предсвязаны, то их произведение J × K тоже предсвязано.

LaTeX

$$$[IsPreconnected(J)] [IsPreconnected(K)] \\Rightarrow IsPreconnected(J \\times K)$$$

Lean4

instance prod [IsPreconnected J] [IsPreconnected K] : IsPreconnected (J × K) :=
  by
  refine .of_any_functor_const_on_obj (fun {a} F ⟨j, k⟩ ⟨j', k'⟩ => ?_)
  exact (any_functor_const_on_obj (Prod.sectL J k ⋙ F) j j').trans (any_functor_const_on_obj (Prod.sectR j' K ⋙ F) k k')

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