# (Topological) Schemes and their induced maps #

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 "`β`

-scheme on `α`

".

This file develops the basic, abstract theory of these schemes and the functions they induce.

## Main Definitions #

`CantorScheme.inducedMap 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,`(inducedMap A).1`

is the domain and`(inducedMap A).2`

is the function.

## Implementation Notes #

We consider end-appending to be the fundamental way to build lists (say on `β`

) inductively,
as this interacts better with the topology on `ℕ → β`

.
As a result, functions like `List.get?`

or `Stream'.take`

do not have their intended meaning
in this file. See instead `PiNat.res`

.

## References #

- [kechris1995] (Chapters 6-7)

## Tags #

scheme, cantor scheme, lusin scheme, approximation.

From a `β`

-scheme on `α`

`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.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A useful strengthening of being antitone is to require that each set contains the closure of each of its children.

## Instances For

If `x`

is in the domain of the induced map of a scheme `A`

,
its image under this map is in each set along the corresponding branch.

A scheme where the children of each set are pairwise disjoint induces an injective map.

A scheme on a metric space has vanishing diameter if diameter approaches 0 along each branch.

## Equations

- CantorScheme.VanishingDiam A = ∀ (x : ℕ → β), Filter.Tendsto (fun (n : ℕ) => EMetric.diam (A (PiNat.res x n))) Filter.atTop (nhds 0)

## Instances For

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.