Topology on SignType

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

instance instTopologicalSpaceSignType : TopologicalSpace SignType

Equations

• instTopologicalSpaceSignType = ⊥

instance instDiscreteTopologySignTypeInstTopologicalSpaceSignType : DiscreteTopology SignType

Equations

• instDiscreteTopologySignTypeInstTopologicalSpaceSignType = instDiscreteTopologySignTypeInstTopologicalSpaceSignType.proof_1

theorem continuousAt_sign_of_pos {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableRel fun x x_1 => x < x_1] [OrderTopology α] {a : α} (h : 0 < a) : ContinuousAt (↑SignType.sign) a

theorem continuousAt_sign_of_neg {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableRel fun x x_1 => x < x_1] [OrderTopology α] {a : α} (h : a < 0) : ContinuousAt (↑SignType.sign) a

theorem continuousAt_sign_of_ne_zero {α : Type u_1} [Zero α] [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : a ≠ 0) : ContinuousAt (↑SignType.sign) a