Definition 7
Tag 0C90, permanent. Cite it as [Bourbaki, Tag 0C90].
General Topology, chapter IX, § 6. Polish spaces, Souslin spaces, Borel sets
A sieve is a sequence C = (C_n, p_n)_{n \geq 0} such that, for each n, C_n is a countable set and p_n is a surjection of C_{n+1} onto C_n.
For each pair of integers m, n such that 0 \leq m \leq n, let p_{mn} denote the identity mapping of C_m onto itself if m = n, and the surjection p_m \circ p_{m+1} \circ \cdots \circ p_{n-1} of C_n onto C_m if m < n. Clearly p_{mq} = p_{mn} \circ p_{nq} whenever m \leq n \leq q, and we may therefore consider the inverse limit L(C) of the family (C_n) with respect to the family of mappings (p_{mn}) (Set Theory, Chapter III, § 7). If each C_n is endowed with the discrete topology, then L(C) is an inverse limit of topological spaces (Chapter I, § 4, no. 4); as such, L(C) is called the topological space associated with the sieve C. L(C) is a closed subspace of the topological product , and it follows immediately that L(C) is a zero-dimensional Polish space (no. 4).
A sifting of a metric space X consists of a sieve C = (C_n, p_n) and for each integer n \geq 0 a mapping \varphi_n of C_n into the set of non-empty closed subsets of X of diameter \leq 2^{-n}, such that:
a) X is the union of the sets \varphi_0(c) as c runs through C_0; b) for each n and each c \in C_n, \varphi_n(c) is the union of the sets \varphi_{n+1}(c'), where c' runs through p_n^{-1}(c).
A sifting is said to be strict if in addition, for each n, the sets \varphi_n(c), as c runs through C_n, are mutually disjoint.
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.
Cited by
Nothing.