[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
refine' (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr _
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ (fun x => 1) =ᶠ[nhds a] ↑SignType.sign
[PROOFSTEP]
rw [Filter.EventuallyEq, eventually_nhds_iff]
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∃ t, (∀ (x : α), x ∈ t → 1 = ↑SignType.sign x) ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
exact ⟨{x | 0 < x}, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
refine' (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr _
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ (fun x => -1) =ᶠ[nhds a] ↑SignType.sign
[PROOFSTEP]
rw [Filter.EventuallyEq, eventually_nhds_iff]
[GOAL]
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∃ t, (∀ (x : α), x ∈ t → -1 = ↑SignType.sign x) ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
exact ⟨{x | x < 0}, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩
[GOAL]
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (↑SignType.sign) a
[PROOFSTEP]
rcases h.lt_or_lt with (h_neg | h_pos)
[GOAL]
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
[PROOFSTEP]
exact continuousAt_sign_of_neg h_neg
[GOAL]
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
[PROOFSTEP]
exact continuousAt_sign_of_pos h_pos
