blob: 50ef6b2b0ddec4805c8677f622a1aa5924ea9635 (
plain)
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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
subseteq : "X is a subset of Y" | \Subseteq
subset : "X is a proper subset of Y" | \Subset
disjoint : "X is disjoint from Y"
inters : "the intersection of the family X"
inter : "the intersection of X and Y" | \Intersection
setminus : "the difference of X and Y" | \Difference
times : "the Cartesian product of X and Y" | \Cartesian
symdiff : "the symmetric difference of X and Y"
bipartitions_of_a_set : "the set of bipartitions of X"
partition : "X is a partition"
partition_refinement : "X is a refinement of Y"
filter : "X is a filter on Y"
principalfilter : "the principal filter on X generated by Y"
maximalfilter : "X is a maximal filter on Y"
relation : "X is a relation"
comparable : "X is comparable with Y with respect to Z"
converse_relation : "the converse of X"
dom : "the domain of X"
ran : "the range of X"
fld : "the field of X"
img : "the image under X of Y"
preimg : "the preimage under X of Y"
upward_closure : "the upward closure with respect to X of Y"
downward_closure : "the downward closure with respect to X of Y"
circ : "the composition of F and G" | \Circ
restrl : "the restriction of X to Y"
rels : "the set of relations from X to Y"
id : "the identity relation on X"
memrel : "the membership relation on X"
subseteqrel : "the subset relation on X"
left_quasireflexive : "X is left quasireflexive"
right_quasireflexive : "X is right quasireflexive"
quasireflexive : "X is quasireflexive"
coreflexive : "X is coreflexive"
reflexive_on : "X is reflexive on Y"
irreflexive : "X is irreflexive"
antisymmetric : "X is antisymmetric"
symmetric : "X is symmetric"
asymmetric : "X is asymmetric"
transitive : "X is transitive"
dense : "X is dense"
quasiconnex : "X is quasiconnex"
connex : "X is connex on Y"
strongly_quasiconnex : "X is strongly quasiconnex"
strongly_connex : "X is strongly connex on Y"
righteuclidean : "X is right Euclidean"
lefteuclidean : "X is left Euclidean"
quotient : "the quotient of X by Y"
equivalence_from_partition : "the equivalence relation induced by partition P on A"
reflexive_closure : "the reflexive closure on X of R"
reflexive_reduction : "the reflexive reduction on X of R"
symmetric_closure : "the symmetric closure of X"
injective : "X is injective"
rightunique : "X is right-unique"
lefttotal : "X is left-total on Y"
righttotal : "X is right-total on Y"
apply : "the value of X at Y"
funs : "the set of functions from X to Y"
inj : "the set of injections from X to Y"
surj : "the set of surjections from X to Y"
bijections : "the set of bijections from X to Y"
fixpoint : "X is a fixed point of Y"
subseteqpreserving : "X is subset-preserving"
suc : "the successor of X"
transitiveset : "X is membership-transitive"
ordinal : "X is an ordinal"
limit_ordinal : "X is a limit ordinal"
successor_ordinal : "X is a successor ordinal"
idempotents : "the idempotents of X"
submagma : "X is a submagma of Y"
left_orbit : "the left orbit of X under Y"
tostrictorder : "the strict part of X"
toorder : "the order on A generated by R"
finite : "X is finite"
cardinality : "X has cardinality Y"
real_sub : "X minus Y"
real_div : "X divided by Y"
real_rationals : "the rational numbers"
real_upper_bound : "X is an upper bound of Y"
real_bounded_above : "X is bounded above"
real_lower_bound : "X is a lower bound of Y"
real_bounded_below : "X is bounded below"
real_bounded : "X is bounded"
real_supremum : "X is a supremum of Y"
real_infimum : "X is an infimum of Y"
real_maximum : "X is a maximum of Y"
real_minimum : "X is a minimum of Y"
intervalclosed : "the closed interval from X to Y"
intervalopen : "the open interval from X to Y"
intervalopen_infinite_left : "the open interval below X"
intervalopen_infinite_right : "the open interval above X"
intervalclosed_infinite_left : "the closed interval below X"
intervalclosed_infinite_right : "the closed interval above X"
initial_segment_naturalsplus : "the initial segment of positive natural numbers up to X"
finite_real_sequence : "X is a finite sequence of real numbers"
infinite_real_sequence : "X is an infinite sequence of real numbers"
partial_sums_sequence : "X is the sequence of partial sums associated with Y"
sum_of_finite_sequence : "X is the sum of Y"
countable : "X is countable"
|
