{'fraction_non_alphanumeric': 0.06394654322831118, 'fraction_numerical': 0.01971031805285949, 'mean_word_length': 3.9830729166666665, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On the computational properties of the uncountability of the real numbers

The uncountability of the real numbers is one of their most basic properties, known (far) outside of mathematics. Cantor's 1874 proof of the uncountability of the real numbers even appears in the very first paper on set theory, i.e. a historical milestone. Despite this famous status and history, the computational properties of the uncountability of the real numbers have not been studied much. In this paper, we study the following computational operation that witnesses that the real numbers not countable: on input a countable set of reals, output a real not in that set. In particular, we formulate a considerable number of operations that are computationally equivalent to the centred operation, working in Kleene's higher-order computability theory based on his S1-S9 computation schemes. Perhaps surprisingly, our equivalent operations involve most basic properties of the Riemann integral and Volterra's early work circa 1881.


Motivation and overview
Like Hilbert ([9]), we believe the infinite to be a central object of study in mathematics. That the infinite comes in 'different sizes' is a relatively new insight, due to Cantor around 1874 ( [6]), in the guise of the uncountability of R, also known simply as Cantor's theorem. Cantor's paper [6] is heralded as the first paper in set theory, complete with its own Wikipedia page [39].
Despite the aforementioned famous status, the computational properties of the uncountability of R have not been studied much. In this paper, we study the following computational operation witnessing that R is not countable: on input a countable set A ⊂ R, output y ∈ R \ A.
In particular, we show that this operation is computationally equivalent to the following ones. Note that a regulated function has left and right limits everywhere, as studied by Bourbaki for Riemann integration (see Section 1.3.3). A full list may be found in Theorem 16. We work in Kleene's higher-order computability theory, based on his S1-S9 computation schemes (see Section 1.3.1). Like in [28], a much weaker notion of computability should suffice, namely based on a fragment of Gödel's T . We note that by [27,Theorem 18], the operations in the above list are hard 1 to compute relative to the usual hierarchy based on comprehension. An explanation for this phenomenon is also in Section 1.3.1. Some of the above operations, including items (iii) and (iv) in the list, stem from Volterra's early work (1881) in the spirit of -but predating-the Baire category theorem, as discussed in Section 1.2.
It should not be a surprise that the above equivalences crucially hinge on our definition of 'countable set', as discussed in detail in Remark 8. In a nutshell, the set theoretic definition of 'countable set' (based on injections or bijections to N) is not suitable for studying regulated functions; our alternative definition (based on unions over N of finite sets) is closer to the way countable sets occur 'in the wild', at least in the context of regulated functions.
Finally, this paper is a spin-off from my project with Dag Normann (University of Oslo) on the logical and computational properties of the uncountable. The interested reader may consult [20, 25,28] for further details on our project.

Volterra's early work and related results
We introduce Volterra's early work from [38] as it pertains to this paper.
First of all, the Riemann integral was groundbreaking for a number of reasons, including its ability to integrate functions with infinitely many points of discontinuity, as shown by Riemann himself ( [29]). A natural question is then 'how discontinuous' a Riemann integrable function can be. In this context, Thomae introduced T : R → R around 1875 in [36, p. 14, §20]): 1 The functional S 2 k from Section 1.3.2 can decide Π 1 k -formulas, but the centred operation is not computable in S 2 k (or their union). Kleene's ∃ 3 from Section 1.3.2 computes the centred operation, but the former also yields full second-order arithmetic.
Thomae's function T is integrable on any interval, but has a dense set of points of discontinuity, namely Q, and a dense set of points of continuity, namely R \ Q.
The perceptive student, upon seeing Thomae's function as in (1), will ask for a function continuous at each rational point and discontinuous at each irrational one. Such a function cannot exist, as is generally proved using the Baire category theorem. However, Volterra in [38] already established this negative result about twenty years before the publication of the Baire category theorem.
Secondly, as to the content of Volterra's paper [38], we find the following theorem on the first page, where a function is pointwise discontinuous if it has a dense set of continuity points.
Theorem 1 (Volterra, 1881) There do not exist pointwise discontinuous functions defined on an interval for which the continuity points of one are the discontinuity points of the other, and vice versa.
Volterra then states two corollaries, of which the following is perhaps well-known in 'popular mathematics' and constitutes the aforementioned negative result.
Corollary 2 (Volterra, 1881) There is no R → R function that is continuous on Q and discontinuous on R \ Q.
Thirdly, we shall study Volterra's theorem and corollary restricted to regulated functions (see Section 1.3.3). The latter kind of functions are automatically 'pointwise discontinuous' in the sense of Volterra.
Fourth, Volterra's results from [38] are generalised in [7,33]. The following theorem is immediate from these generalisations. In conclusion, the perceptive reader has already noted that most equivalent principles have a 'Baire category theorem' flavour to them. In particular, the intuitive notion of 'small or negligible set' can be formalised in at least two (fairly independent) ways, namely based on 'measure' and 'density/meagre'. The equivalences in this paper do not (and we believe cannot) involve the former, but heavily depend on the latter.

Preliminaries and definitions
We briefly introduce Kleene's higher-order computability theory in Section 1.3.1. We introduce some essential axioms (Section 1.3.2) and definitions (Section 1.3.3). A full introduction may be found in e.g. [25, §2]. Since Kleene's computability theory borrows heavily from type theory, we shall often use common notations from the latter; for instance, the natural numbers are type 0 objects, denoted n 0 or n ∈ N. Similarly, elements of Baire space are type 1 objects, denoted f ∈ N N or f 1 . An overview of this kind of notations is in Section 3.

Kleene's computability theory
Our main results are in computability theory and we make our notion of 'computability' precise as follows.
(I) We adopt ZFC, i.e. Zermelo-Fraenkel set theory with the Axiom of Choice, as the official metatheory for all results, unless explicitly stated otherwise. (II) We adopt Kleene's notion of higher-order computation as given by his nine clauses S1-S9 (see [15,Ch. 5] or [11]) as our official notion of 'computable'.
We mention that S1-S8 are rather basic and merely introduce a kind of higherorder primitive recursion with higher-order parameters. The real power comes from S9, which essentially hard-codes the recursion theorem for S1-S9-computability in an ad hoc way. By contrast, the recursion theorem for Turing machines is derived from first principles in [35].
On a historical note, it is part of the folklore of computability theory that many have tried (and failed) to formulate models of computation for objects of all finite types in which one derives the recursion theorem in a natural way. For this reason, Kleene ultimately introduced S1-S9, which were initially criticised for their ad hoc nature, but eventually received general acceptance nonetheless. On a related note, an equivalent-but-more-elegant λ-calculus formulation of S1-S9computability based on fixed point operators may be found in [28]; an additional advantage of the framework from [28] is that it accommodates partial objects.
We refer to [15,28] for a (more) thorough overview of higher-order computability theory. We do mention the distinction between 'normal' and 'nonnormal' functionals based on the following definition from [15, §5.4]. We only make use of ∃ n for n = 2, 3, as defined in Section 1.3.2.
Definition 4 For n ≥ 2, a functional of type n is called normal if it computes Kleene's ∃ n following S1-S9, and non-normal otherwise.
In this paper, we greatly extend the study of the uncountability of R mentioned in the fifth item; the operations sketched in Section 1 are all non-normal, in that they do not even compute Kleene's ∃ 2 from Section 1.3.2.

Some comprehension functionals
In Turing-style computability theory, computational hardness is measured in terms of where the oracle set fits in the well-known comprehension hierarchy. For this reason, we introduce some axioms and functionals related to higher-order comprehension in this section. We are mostly dealing with conventional comprehension here, i.e. only parameters over N and N N are allowed in formula classes like Π 1 k and Σ 1 k . First of all, the functional ϕ 2 , also called Kleene's quantifier ∃ 2 , as in (∃ 2 ) is clearly discontinuous at f = 11 . . . ; in fact, ∃ 2 is (computationally) equivalent to the existence of F : R → R such that F (x) = 1 if x > R 0, and 0 otherwise via Grilliot's trick (see [13, §3]).
By definition, the Suslin functional S 2 can decide whether a Σ 1 1 -formula as in the left-hand side of (S 2 ) is true or false. We similarly define the functional S 2 k which decides the truth or falsity of Σ 1 k -formulas from L 2 . We note that the operators ν n from [5, p. 129] are essentially S 2 n strengthened to return a witness (if existant) to the Σ 1 n -formula at hand. Thirdly, the functional E 3 clearly computes ∃ 2 and S 2 k for any k ∈ N: The functional from (∃ 3 ) is also called Kleene's quantifier ∃ 3 , and we use the same -by now obvious-convention for other functionals.
In conclusion, the operations sketched in Section 1 are computable in ∃ 3 but not in any S 2 k , as noted in Footnote 1 and which immediately follows from [27,Theorem 18]. Many non-normal functionals exhibit the same 'computational hardness' and we merely view this as support for the development of a separate scale for classifying non-normal functionals.

Some definitions
We introduce some definitions needed in the below, mostly stemming from mainstream mathematics.
First of all, we shall study the following notions of weak continuity, going back (at least) to the days of Baire and Volterra.
Definition 5 For f : [0, 1] → R, we have the following definitions: Scheeffer studies discontinuous regulated functions in [32] arround 1884 (without using the term 'regulated'), while Bourbaki develops Riemann integration based on regulated functions in [3]. An interesting observation about regular functions and continuity is as follows.
Remark 6 (Continuity and regulatedness) First of all, as discussed in [13, §3], the local equivalence for functions on Baire space between sequential and 'epsilon-delta' continuity cannot be proved in ZF. By [26,Theorem 3.32], this equivalence for regulated functions is provable in ZF (and much weaker systems). Secondly, µ 2 readily computes the left and right limits of regulated f : [0, 1] → R. In this way, the formula 'f is continuous at . The usual 'epsilondelta' definition of continuity involves quantifiers over R, i.e. the previous equality is much simpler and more elementary.
Secondly, we also need the notion of 'intermediate value property', also called the 'Darboux property'.
any left (resp. right) cluster value y of f at x and z ∈ R strictly between y By definition, a point of continuity is also a Darboux point, but not vice versa. Thirdly, as suggested in Section 1, the set-theoretic definition of countable set is not suitable for the study of regulated functions (in computability theory). We present our alternative notion in Definition 11, which amounts to 'unions over N of finite sets'. We first provide some motivation in Remark 8. We assume subsets of R are given by their characteristic functions.

Remark 8 (Countable sets by any other name)
First of all, we have previously investigated the computational properties of the Jordan decomposition theorem in [27,28]. In the latter, a central object of study is as follows: a functional E that on input A ⊂ [0, 1] and Y : [0, 1] → N such that Y is injective (or bijective) on A, outputs a sequence of reals listing all reals in A.
We stress that the functional E crucially has two inputs: a countable set A ⊂ [0, 1] and a function Y : [0, 1] → N witnessing that A is countable. Indeed, omitting the second input from E yields a choice function well-known from the Axiom of Choice. However, such functions lack any and all computational content (even in very weak instances: see [24]). Thus, the functional E is not a meaningful object of study in computability theory unless we include the second input Y . Secondly, consider the following sets definable via ∃ 2 , for regulated f : [0, 1] → R: Clearly, A = ∪ n∈N A n collects all points in (0, 1) where f is discontinuous; this set is central to many proofs involving regulated functions (see e.g. [1, Thm. 0.36]). Now, that A n is finite follows by a standard 2 compactness argument. However, while A is then countable, we are unable to construct an injection from A to N (let alone a bijection), even assuming S 2 m . Similarly, for a set A ⊂ R without limit points, A ∩ [−n, n] is finite for any n ∈ N, yet we are again unable to construct an injection from A to N, even assuming S 2 m . In conclusion, the countable set A in (2) is central to many proofs involving regulated functions, but it seems we cannot (in general) construct an injection from A to N. However, this injection is a crucial input of the functional E as omitting it gives rise to a choice function from the Axiom of Choice.
Besides pointing out a problem with the usual definition of countable set, Remark 8 also suggests an alternative, more suitable, definition of countable set, namely 'union over N of finite sets'. We now introduce the 'usual' definitions of countable set (Definitions 9 and 10), and our alternative one (Definition 11).

Definition 9 [Enumerable sets of reals] A set
This definition reflects the RM-notion of 'countable set' from [34, V.4.2]. We note that given µ 2 from Section 1.3.2, we may replace the final implication in Definition 9 by an equivalence. One sometimes finds 'denumerable' in the literature to describe Definition 9.
The first part of Definition 10 is from Kunen's set theory textbook ([14, p. 63]) and the second part is taken from Hrbacek-Jech's set theory textbook [10] (where the term 'countable' is used instead of 'strongly countable'). For the rest of this paper, 'strongly countable' and 'countable' shall exclusively refer to Definition 10, except when explicitly stated otherwise.
Definition 11 A set A ⊂ R is weakly countable if there is a height H : R → N for A, i.e. for all n ∈ N, A n := {x ∈ A : H(x) < n} is finite.
We note that the notion of 'height' is mentioned in e.g. [16, p. 33] and [37], from whence we took this notion. The following remark is crucial for the below.
Remark 12 (Inputs and heights) Similar to the functional E in Remark 8, a functional defined on weakly countable sets always takes two inputs: the set A ⊂ R and the height H : R → N. We note that given a sequence of finite sets (X n ) n∈N in R, a height can be defined as H(x) := (µn)(x ∈ X n ) using Feferman's µ 2 . A set is therefore weakly countable iff it is the union over N of finite sets. In particular, the set A = ∪ n∈N A n as defined in (2) has a height H A (x) := (µn)(x ∈ A n ), which is crucial for the results in Section 2.2.

Main results
We establish the results sketched in Section 1. We generally assume ∃ 2 from Section 1.3.1 to avoid the technical details involved in the representation of sets and real numbers. Given the hardness of the operations from Section 1, as noted in Footnote 1 and Section 1.3.2, this seems like a weak assumption.

Introduction
The uncountability of R can be studied in numerous guises in higher-order computability theory. For instance, the following notions are from [25,27], where it is also shown that many extremely basic operations compute these realisers. Clearly, the realisers in Definition 13 are based on the 'set theoretic' definition of countability. As discussed in Remark 8, the notion of weak countability (Definition 11) seems to be have better, suggesting the following stronger notion.

Definition 14 (Strong Cantor realiser) A strong Cantor realiser is any functional that on input a weakly countable
Following Remark 12, a strong Cantor realiser takes as input a countale set and its height as in Definition 11. Modulo ∃ 2 , this amounts to an input consisting of a sequence (X n ) n∈N of finite sets in [0, 1] and an output y ∈ [0, 1] \ ∪ n∈N X n . The reader will observe that a strong Cantor realiser computes a normal one. Any (weak, strong, or normal) Cantor realiser witnesses the extremely basic idea that removing a countable set from an uncountable one, there is at least one element left. Nonetheless, the functionals S 2 k from Section 1.3.2, which decide Π 1 k -formulas, cannot compute a weak Cantor realiser ( [27,Theorem 18]). We stress that (strong, weak, or normal) Cantor realisers are partial objects: they provide the required output y ∈ [0, 1] \ A when the inputs are given as in their respective specification. If the inputs are not according to the specification, the output may be undefined or may be some real number. As noted in Section 1.3.1, there is an equivalent formulation of Kleene's S1-S9 schemes that accommodates partial objects.
We show in Section 2.2 that many operations on regulated functions are computationally equivalent to strong Cantor realisers. This provides additional justification for the introduction of our new notion of weak countability.

Computational equivalences for strong Cantor realisers
In this section, we show that many operations on regulated functions are computationally equivalent to strong Cantor realisers. We recall that subsets of R are given by characteristic functions.
First of all, various natural functionals compute a strong Cantor realiser.
The second item computes the third item by [22,Theorem 6.5]. Regarding the third item, O n := [0, 1] \ ∪ k≤n X k is (trivially) dense and open. Clearly any y ∈ ∩ n∈N O n by definition satisfies y ∈ [0, 1]\ ∪ n∈N X n , i.e. a realiser for the Baire category theorem computes a strong Cantor realiser.
⊓ ⊔ Secondly, we have the following theorem. Regarding item (k), the property 'x is a local strict 3 maximum of f ' does not seem to be decidable given ∃ 2 for (general) regulated f , in contrast to Remark 6. We also note that items (f) and (g) are based on Volterra's Theorem 1 and Corollary 2, while item (h) is based on the associated generalisation as in Theorem 3, and sports a certain robustness.

Theorem 16
The following are computationally equivalent modulo ∃ 2 .  Proof. First of all, assume item (b) and let X := ∪ n∈N X n be the union of finite sets X n ⊂ [0, 1] and define h as follows: x ∈ X n and n is the least such number .
Since ∪ k≤n X k is finite for all n ∈ N, we observe that h is regulated, in particular 0 Secondly, assume item (c) and note that if f : [0, 1] → R is continuous at y ∈ [0, 1], we can use µ 2 to find N ∈ N such that (∀q ∈ B(y, 1 2 N ) ∩ Q ∩ [0, 1])(|f (y) − f (q)| < 1 2 ); this readily yields a, b ∈ [0, 1] as required by item (b). We note that item (e) immediately yields item (c), while the reversal readily follows by rescaling. Moreover, item (c) implies item (d); applying the latter to h as in (3), we observe that any point y ∈ [0, 1] where h is quasi-or lower semi-continuous or Darboux, is such that y ∈ [0, 1]\∪ n∈N X n , i.e. item (a) follows.
Thirdly, assume item (f) and fix regulated f : [0, 1] → R. The following case distinction is decidable using ∃ 2 : In the first case, use µ 2 to find this rational. In the second case, the output of item (f) must be x ∈ [0, 1] \ Q such that f is continuous at x. In each case, we have a point of continuity for f , i.e. item (c) follows.
Fourth, assume item (a) and fix regulated f : In case f is continuous at all q ∈ [0, 1] ∩ Q, let (q m ) m∈N be an enumeration of Q ∩ [0, 1]. Now consider the following set which is finite by Footnote 2. Now use the strong Cantor realiser to find y ∈ [0, 1]\ ∪ n∈N Y n , where Y n = X n ∪ {q n }. Then f must be continuous at y ∈ [0, 1] \ Q and item (f) follows.
Fifth, assume item (i) and let h be as in (3). Since h is regulated, it is Riemann integrable, with Seventh, consider item (k) and note that h as in (3) is regulated with only removable discontinuities. Now, the set X = ∪ n∈N X n consists of the local strict maxima of h, i.e. item (k) yields a strong Cantor realiser. For the reversal, ∃ 2 computes a functional M such that M (g, a, b) is a maximum of g ∈ C([0, 1]) on [a, b] ⊂ [0, 1] (see [13, §3]), i.e. (∀y ∈ [a, b])(g(y) ≤ g(M (g, a, b))). Using the functional M , one readily shows that 'x is a strict local maximum of g' is decidable 4 given ∃ 2 , for g continuous on [0,1]. Now let f : [0, 1] → R be regulated and with only removable discontinuities. Use ∃ 2 to definef : [0, 1] → R as follows:f (x) := f (x+) for x ∈ [0, 1) andf (1) = f (1−). By definition,f is continuous on [0, 1], and ∃ 2 computes a (continuous) modulus of continuity, which follows in the same way as for Baire space (see e.g. [12, §4]). In case f is discontinuous at x ∈ [0, 1], the latter point is a strict local maximum of f if and only if f (x) > f (x+) (or f (x) > f (x−) in case x = 1). Note that µ 2 (together with a modulus of continuity forf ) readily yields N f,x ∈ N such that (∀y ∈ B(x, 1 2 N f,x ))(f (y) < f (x)), in case x is a strict local maximum of f . In case f is continuous at x ∈ [0, 1], we can use ∃ 2 to decide whether x is a local strict maximum off . By Footnote 4, µ 2 again yields N f,x ∈ N such that (∀y ∈ B(x, 1 2 N ))(f (y) <f (x))), in case x is a strict local maximum off . Now consider the following set: x is a strict local maximum off or f with n ≥ N f,x }.
Then A n has finitely elements as strict local maxima cannot be 'too close'. Hence, a strong Cantor realiser yields y ∈ [0, 1] \ ∪ n∈N A n , which is not a local maximum of f , i.e. item (k) follows.
Next, item (h) implies (f) as D = Q is trivially (weakly or strongly) countable. To derive item (h) from item (a), consider X n as in (4) and assume D = ∪ n∈N D n is dense, where D n is finite for all n ∈ N. Note that µ 2 can find q ∈ [0, 1] ∩ D ∩ Q with f (q+) = f (q)∨f (q−) = f (q), if such rational exists. In case f is continuous at all q ∈ [0, 1] ∩ D ∩ Q, use a strong Cantor realiser to find y ∈ [0, 1] \ ∪ n∈N Z n , where Z n = X n ∪ D n . By definition, y ∈ [0, 1] \ D and f is continuous at y.
Finally, assume item (g) and note that Thomae's function from (1) is regulated as the left and right limits are 0. Hence, we obtain item (f), as Thomae's function is continuous on R \ Q and discontinuous on Q. To obtain item (g) from a strong Cantor realiser, let f, g : [0, 1] be regulated and consider the finite set X n as in (4). Let Y n be the same set for g. Then use a strong Cantor realiser to obtain y ∈ [0, 1] \ ∪ n∈N (X n ∪ Z n ) . By definition, f and g are continuous at y, i.e. item (g) follows.
⊓ ⊔ Regarding item (k), one readily shows that the following functional is computationally equivalent to Ω from Theorem 15. Note that the set of strict local maxima is countable for any R → R-function by [31, p. 261, Theorem (1.1)].
-A functional that on input regulated f : [0, 1] → R with only removable discontinuities, outputs an enumeration of all strict local maxima.
In conclusion, we have established a number of equivalences for strong Cantor realisers, while many more variations are possible.

Some details of Kleene's computability theory
Kleene's computability theory borrows heavily from type theory and higherorder arithmetic. We briefly sketch some of the associated notions.
First of all, Kleene's S1-S9 schemes define 'Ψ is computable in terms of Φ' for objects Φ, Ψ of any finite type. Now, the collection of all finite types T is defined by the following two clauses: where 0 is the type of natural numbers, and σ → τ is the type of mappings from objects of type σ to objects of type τ . In this way, 1 ≡ 0 → 0 is the type of functions from numbers to numbers, and n + 1 ≡ n → 0. We view sets X of type σ objects as given by characteristic functions F σ→0 X . Secondly, for variables x ρ , y ρ , z ρ , . . . of any finite type ρ ∈ T, types may be omitted when they can be inferred from context. The constants include the type 0 objects 0, 1 and < 0 , + 0 , × 0 , = 0 which are intended to have their usual meaning as operations on N. Equality at higher types is defined in terms of '= 0 ' as follows: for any objects x τ , y τ , we have if the type τ is composed as τ ≡ (τ 1 → . . . → τ k → 0). Thirdly, we introduce the usual notations for common mathematical notions, like real numbers, as also can be found in [13].

Definition 17 (Real numbers and related notions)
a. Natural numbers correspond to type zero objects, and we use 'n 0 ' and 'n ∈ N' interchangeably. Rational numbers are defined as signed quotients of natural numbers, and 'q ∈ Q' and '< Q ' have their usual meaning. b. Real numbers are coded by fast-converging Cauchy sequences q (·) : N → Q, i.e. such that (∀n 0 , i 0 )(|q n −q n+i | < Q 1 2 n ). We use Kohlenbach's 'hat function' from [13, p. 289] to guarantee that every q 1 defines a real number. c. We write 'x ∈ R' to express that x 1 := (q 1 (·) ) represents a real as in the previous item and write [x](k) := q k for the k-th approximation of x. d. Two reals x, y represented by q (·) and r (·) are equal, denoted x = R y, if (∀n 0 )(|q n − r n | ≤ 2 −n+1 ). Inequality '< R ' is defined similarly. We sometimes omit the subscript 'R' if it is clear from context. e. Functions F : R → R are represented by Φ 1→1 mapping equal reals to equal reals, i.e. extensionality as in (∀x, y ∈ R)(x = R y → Φ(x) = R Φ(y)). f. The relation 'x ≤ τ y' is defined as in (5) but with '≤ 0 ' instead of '= 0 '. Binary sequences are denoted 'f 1 , g 1 ≤ 1 1', but also 'f, g ∈ C' or 'f, g ∈ 2 N '. Elements of Baire space are given by f 1 , g 1 , but also denoted 'f, g ∈ N N '. g. Sets of type ρ objects X ρ→0 , Y ρ→0 , . . . are given by their characteristic functions F ρ→0 X ≤ ρ→0 1, i.e. we write 'x ∈ X' for F X (x) = 0 1.
For completeness, we list the following notational convention for finite sequences.