α : 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
α : 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
refine' (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr _
α : 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
α : 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
rw [Filter.EventuallyEq, eventually_nhds_iff]
no goals
α : 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
exact ⟨{ x | 0 < x }, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩