-
Notifications
You must be signed in to change notification settings - Fork 16
/
order_theory.theory.txt
66 lines (50 loc) · 4.37 KB
/
order_theory.theory.txt
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
57
58
59
60
61
62
63
64
65
66
ORDER_THEORY
ORDER THEORY ==> #Math branch about order
PARTIAL ORDER ==> #Binary relation that is:
# - transitive
# - antisymmetric
# - homogeneous
STRICT PARTIAL ORDER ==> #Partial order that is not reflexive.
#Also named "irreflexive", "strong".
#E.g. <
NON-STRICT PARTIAL ORDER ==> #Partial order that is reflexive.
#Also named "reflexive", "weak".
#E.g. <=
TOTAL ORDER ==> #Non-strict partial order where every element is strongly connected ("total")
GREATEST ELEMENT ==> #Also named "top" or "unit"
#Noted ⊤ or 1
#Value of a given set >= any others
LEAST ELEMENT ==> #Also named "bottom" or "zero"
#Noted ⊥ or 0
#Inverse of greatest element
MAXIMAL ELEMENT ==> #Value of a given set not < any others
#If set is:
# - totally ordered: same as greatest element
# - partially ordered: there is 0-1 greatest element, but can be 0-n maximal elements
MINIMAL ELEMENT ==> #Inverse of maximal element
MAXIMUM|MINIMUM ==> #Maximal|minimal element of a totally ordered set, i.e. also greatest|least element
EXTREMUM ==> #Maximum or minimum
ABSOLUTE MAXIMUM|MINIMUM ==> #Also named "global maximum|minimum"
#Maximal|minimal element of a function's codomain
RELATIVE MAXIMUM|MINIMUM ==> #Also named "local maximum|minimum"
#Like abolute maximum but only for a subset of the function's domain+codomain
TIGHT UPPER BOUND ==> #Also named "supremum", "join" or "least|sharp|optimal upper bound"
#Lowest value >= any value of a given set
#Not always same as greatest|maximal element
# - e.g. infinite sets have no greatest|maximal element, but can have tight upper bound
#But:
# - greatest element is always tight upper bound
# - one maximal element is always tight upper bound
TIGHT LOWER BOUND ==> #Also named "infimum", "meet" or "greatest|sharp|optimal lower bound"
#Inverse of tight upper bound.
UPPER BOUND ==> #Also named "majorant"
#Any value >= any value of a given set
#That value is said to "majorize"/"bound from above" the set.
LOWER BOUND ==> #Also named "minorant"
#Inverse of upper bound
#That value is said to "minorize"/"bound from below" the set.
FUNCTION UPPER|LOWER BOUND ==> #Upper|lower bound of a function's codomain.
UPPER|LOWER BOUNDING FUNCTION ==> #Function f where any f(x) >= g(x), i.e. f is upper bound of g
#Or inverse for lower bound