totallyDisconnectedSpace — Mathlib

English

If each β(a) is totally disconnected, then the product space ∀ a, β(a) is totally disconnected.

Русский

Если каждое β(a) не соединяется, то произведение пространств ∀ a, β(a) также распр. несоединённо.

LaTeX

$$$\Big(\forall a, TotallyDisconnectedSpace(\beta(a))\Big) \Rightarrow TotallyDisconnectedSpace(\forall a, \beta(a))$$$

Lean4

instance totallyDisconnectedSpace {α : Type*} {β : α → Type*} [∀ a, TopologicalSpace (β a)]
    [∀ a, TotallyDisconnectedSpace (β a)] : TotallyDisconnectedSpace (∀ a : α, β a) :=
  ⟨fun t _ h2 =>
    have this : ∀ a, IsPreconnected ((fun x : ∀ a, β a => x a) '' t) := fun a =>
      h2.image (fun x => x a) (continuous_apply a).continuousOn
    fun x x_in y y_in => funext fun a => (this a).subsingleton ⟨x, x_in, rfl⟩ ⟨y, y_in, rfl⟩⟩

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