English
The sigma-type of extremally disconnected spaces is extremally disconnected.
Русский
Сигма-произведение экстремально разобщимых пространств также экстремально разобщимо.
LaTeX
$$$$ \\text{ExtremallyDisconnected} (\\Sigma i, X_i). $$$$
Lean4
/-- The sigma-type of extremally disconnected spaces is extremally disconnected. -/
instance instExtremallyDisconnected {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
[h₀ : ∀ i, ExtremallyDisconnected (X i)] : ExtremallyDisconnected (Σ i, X i) :=
by
constructor
intro s hs
rw [isOpen_sigma_iff] at hs ⊢
intro i
rcases h₀ i with ⟨h₀⟩
suffices h : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
by
rw [h]
exact h₀ _ (hs i)
apply IsOpenMap.preimage_closure_eq_closure_preimage
· intro U _
rw [isOpen_sigma_iff]
intro j
by_cases ij : i = j
· rwa [← ij, sigma_mk_preimage_image_eq_self]
· rw [sigma_mk_preimage_image' ij]
exact isOpen_empty
· fun_prop
