case inl
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (↑SignType.sign) a

case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (↑SignType.sign) a
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (↑SignType.sign) a
rcases h.lt_or_lt with (h_neg | h_pos)
no goals
case inl
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (↑SignType.sign) a
exact continuousAt_sign_of_neg h_neg
no goals
case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (↑SignType.sign) a
exact continuousAt_sign_of_pos h_pos