# (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.

noncomputable def CantorScheme.inducedMap {β : Type u_1} {α : Type u_2} (A : List βSet α) :
(s : Set (β)) × (sα)

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
def CantorScheme.Antitone {β : Type u_1} {α : Type u_2} (A : List βSet α) :

A scheme is antitone if each set contains its children.

Equations
Instances For
def CantorScheme.ClosureAntitone {β : Type u_1} {α : Type u_2} (A : List βSet α) [] :

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

Equations
Instances For
def CantorScheme.Disjoint {β : Type u_1} {α : Type u_2} (A : List βSet α) :

A scheme is disjoint if the children of each set of pairwise disjoint.

Equations
Instances For
theorem CantorScheme.map_mem {β : Type u_1} {α : Type u_2} {A : List βSet α} (x : .fst) (n : ) :
.snd x A (PiNat.res (x) n)

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.

theorem CantorScheme.ClosureAntitone.antitone {β : Type u_1} {α : Type u_2} {A : List βSet α} [] (hA : ) :
theorem CantorScheme.Antitone.closureAntitone {β : Type u_1} {α : Type u_2} {A : List βSet α} [] (hanti : ) (hclosed : ∀ (l : List β), IsClosed (A l)) :
theorem CantorScheme.Disjoint.map_injective {β : Type u_1} {α : Type u_2} {A : List βSet α} (hA : ) :

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

def CantorScheme.VanishingDiam {β : Type u_1} {α : Type u_2} (A : List βSet α) :

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

Equations
Instances For
theorem CantorScheme.VanishingDiam.dist_lt {β : Type u_1} {α : Type u_2} {A : List βSet α} (hA : ) (ε : ) (ε_pos : 0 < ε) (x : β) :
∃ (n : ), yA (), zA (), dist y z < ε
theorem CantorScheme.VanishingDiam.map_continuous {β : Type u_1} {α : Type u_2} {A : List βSet α} [] [] (hA : ) :

A scheme with vanishing diameter along each branch induces a continuous map.

theorem CantorScheme.ClosureAntitone.map_of_vanishingDiam {β : Type u_1} {α : Type u_2} {A : List βSet α} [] (hdiam : ) (hanti : ) (hnonempty : ∀ (l : List β), Set.Nonempty (A l)) :
.fst = Set.univ

A scheme on a complete space with vanishing diameter such that each set contains the closure of its children induces a total map.