instPreconnectedSpaceForall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance [∀ i, TopologicalSpace (X i)] [∀ i, PreconnectedSpace (X i)] : PreconnectedSpace (∀ i, X i) :=
  ⟨by rw [← pi_univ univ]; exact isPreconnected_univ_pi fun i => isPreconnected_univ⟩

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