Topology on SignType

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

@[instance_reducible]

instance instTopologicalSpaceSignType : TopologicalSpace SignType

Equations

• instTopologicalSpaceSignType = ⊥

instance instDiscreteTopologySignType : DiscreteTopology SignType

theorem continuousAt_sign_of_pos {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableLT α] [OrderTopology α] {a : α} (h : 0 < a) : ContinuousAt (⇑SignType.sign) a

theorem continuousAt_sign_of_neg {α : Type u_1} [Zero α] [TopologicalSpace α] [PartialOrder α] [DecidableLT α] [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

theorem IsPreconnected.sign_eq_of_continuousOn {α : Type u_1} [Zero α] [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {X : Type u_2} [TopologicalSpace X] {f : X → α} {s : Set X} (hs : IsPreconnected s) (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : SignType.sign (f x) = SignType.sign (f y)