extremallyDisconnected_of_homeo — Mathlib

English

If X is extremally disconnected and there is a homeomorphism X ≃ₜ Y, then Y is extremally disconnected.

Русский

Если X экстремально разобщимо и существует гомеморфизм X ≃ₜ Y, то Y тоже экстремально разобщимо.

LaTeX

$$$$ \\text{If } X \\text{ is extremally disconnected and } X \\cong_t Y, \\text{ then } Y \\text{ is extremally disconnected}. $$$$

Lean4

theorem extremallyDisconnected_of_homeo {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [ExtremallyDisconnected X] (e : X ≃ₜ Y) : ExtremallyDisconnected Y where
  open_closure U
    hU := by
    rw [e.symm.isInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage]
    exact ExtremallyDisconnected.open_closure _ (e.symm.isOpen_image.mpr hU)

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