# Topology on `SignType` #

This file gives `SignType` the discrete topology, and proves continuity results for `SignType.sign` in an `OrderTopology`.

source
instance instTopologicalSpaceSignType :
TopologicalSpace SignType
Equations

- instTopologicalSpaceSignType = ⊥

source
instance instDiscreteTopologySignType :
DiscreteTopology SignType
source
theorem continuousAt_sign_of_pos {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableLT α] [OrderTopology α] {a : α} (h : 0 < a) :
ContinuousAt (⇑SignType.sign) a
source
theorem continuousAt_sign_of_neg {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableLT α] [OrderTopology α] {a : α} (h : a < 0) :
ContinuousAt (⇑SignType.sign) a
source
theorem continuousAt_sign_of_ne_zero {α : Type u_1} [Zero α] [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : a ≠ 0) :
ContinuousAt (⇑SignType.sign) a