-
Notifications
You must be signed in to change notification settings - Fork 273
/
Sign.lean
56 lines (39 loc) · 1.82 KB
/
Sign.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
/-
Copyright (c) 2022 Joseph Myers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Myers
-/
import Mathlib.Data.Sign
import Mathlib.Topology.Order.Basic
#align_import topology.instances.sign from "leanprover-community/mathlib"@"4c19a16e4b705bf135cf9a80ac18fcc99c438514"
/-!
# Topology on `SignType`
This file gives `SignType` the discrete topology, and proves continuity results for `SignType.sign`
in an `OrderTopology`.
-/
instance : TopologicalSpace SignType :=
⊥
instance : DiscreteTopology SignType :=
⟨rfl⟩
variable {α : Type*} [Zero α] [TopologicalSpace α]
section PartialOrder
variable [PartialOrder α] [DecidableRel ((· < ·) : α → α → Prop)] [OrderTopology α]
theorem continuousAt_sign_of_pos {a : α} (h : 0 < a) : ContinuousAt SignType.sign a := by
refine' (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr _
rw [Filter.EventuallyEq, eventually_nhds_iff]
exact ⟨{ x | 0 < x }, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩
#align continuous_at_sign_of_pos continuousAt_sign_of_pos
theorem continuousAt_sign_of_neg {a : α} (h : a < 0) : ContinuousAt SignType.sign a := by
refine' (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr _
rw [Filter.EventuallyEq, eventually_nhds_iff]
exact ⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩
#align continuous_at_sign_of_neg continuousAt_sign_of_neg
end PartialOrder
section LinearOrder
variable [LinearOrder α] [OrderTopology α]
theorem continuousAt_sign_of_ne_zero {a : α} (h : a ≠ 0) : ContinuousAt SignType.sign a := by
rcases h.lt_or_lt with (h_neg | h_pos)
· exact continuousAt_sign_of_neg h_neg
· exact continuousAt_sign_of_pos h_pos
#align continuous_at_sign_of_ne_zero continuousAt_sign_of_ne_zero
end LinearOrder