theorem IsHomeomorph.irreducibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) [IrreducibleSpace X] : IrreducibleSpace Y

theorem IsHomeomorph.irreducibleSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) : IrreducibleSpace X ↔ IrreducibleSpace Y

theorem IsHomeomorph.connectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) [ConnectedSpace X] : ConnectedSpace Y