instPreconnectedSpaceProd — Mathlib

English

If each X_i is a preconnected space, then the product ∏_i X_i is preconnected.

Русский

Если для каждого i пространство X_i предсвязано, то произведение ∏_i X_i предсвязано.

LaTeX

$$$$\\text{PreconnectedSpace}(\\prod_{i} X_i)$$$$

Lean4

instance [TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] : PreconnectedSpace (α × β) :=
  ⟨by
    rw [← univ_prod_univ]
    exact isPreconnected_univ.prod isPreconnected_univ⟩

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