(Topological) Schemes and their induced maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In topology, and especially descriptive set theory, one often constructs functions
(ℕ → β) → α,
where α is some topological space and β is a discrete space, as an appropriate limit of some map
list β → set α. We call the latter type of map a "
This file develops the basic, abstract theory of these schemes and the functions they induce.
Main Definitions #
cantor_scheme.induced_map A: The aforementioned "limit" of a scheme
A : list β → set α. This is a partial function from
ℕ → βto
a, implemented here as an object of type
Σ s : set (ℕ → β), s → α. That is,
(induced_map A).1is the domain and
(induced_map A).2is the function.
Implementation Notes #
We consider end-appending to be the fundamental way to build lists (say on
as this interacts better with the topology on
ℕ → β.
As a result, functions like
stream.take do not have their intended meaning
in this file. See instead
- [Kec95] (Chapters 6-7)
scheme, cantor scheme, lusin scheme, approximation.
A, we define a partial function from
(ℕ → β) to
which sends each infinite sequence
x to an element of the intersection along the
branch corresponding to
x, if it exists.
We call this the map induced by the scheme.
A useful strengthening of being antitone is to require that each set contains the closure of each of its children.
x is in the domain of the induced map of a scheme
its image under this map is in each set along the corresponding branch.
A scheme on a metric space has vanishing diameter if diameter approaches 0 along each branch.
A scheme with vanishing diameter along each branch induces a continuous map.
A scheme on a complete space with vanishing diameter such that each set contains the closure of its children induces a total map.