def Homeomorph.OfDiscrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [DiscreteTopology X] [TopologicalSpace Y] [DiscreteTopology Y] (f : X ≃ Y) : X ≃ₜ Y

Equations

• Homeomorph.OfDiscrete f = { toEquiv := f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem IsHomeomorph.equiv_of_discreteTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [DiscreteTopology X] [TopologicalSpace Y] [DiscreteTopology Y] (f : X ≃ Y) : IsHomeomorph ⇑f

A bijection between discrete topoligical spaces is a homeomorpism.