# mathlib3documentation

topology.metric_space.cantor_scheme

# (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 "β-scheme on α".

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).1 is the domain and (induced_map 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.nth or stream.take do not have their intended meaning in this file. See instead pi_nat.res.

## Tags #

scheme, cantor scheme, lusin scheme, approximation.

noncomputable def cantor_scheme.induced_map {β : 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
@[protected]
def cantor_scheme.antitone {β : Type u_1} {α : Type u_2} (A : list β set α) :
Prop

A scheme is antitone if each set contains its children.

Equations
def cantor_scheme.closure_antitone {β : Type u_1} {α : Type u_2} (A : list β set α)  :
Prop

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

Equations
@[protected]
def cantor_scheme.disjoint {β : Type u_1} {α : Type u_2} (A : list β set α) :
Prop

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

Equations
theorem cantor_scheme.map_mem {β : Type u_1} {α : Type u_2} {A : list β set α} (x : .fst)) (n : ) :
A 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.

@[protected]
theorem cantor_scheme.closure_antitone.antitone {β : Type u_1} {α : Type u_2} {A : list β set α}  :
@[protected]
theorem cantor_scheme.antitone.closure_antitone {β : Type u_1} {α : Type u_2} {A : list β set α} (hanti : cantor_scheme.antitone A) (hclosed : (l : list β), is_closed (A l)) :
theorem cantor_scheme.disjoint.map_injective {β : Type u_1} {α : Type u_2} {A : list β set α} (hA : cantor_scheme.disjoint A) :

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

def cantor_scheme.vanishing_diam {β : Type u_1} {α : Type u_2} (A : list β set α)  :
Prop

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

Equations
theorem cantor_scheme.vanishing_diam.dist_lt {β : Type u_1} {α : Type u_2} {A : list β set α} (hA : cantor_scheme.vanishing_diam A) (ε : ) (ε_pos : 0 < ε) (x : β) :
(n : ), (y : α), y A n) (z : α), z A n) < ε
theorem cantor_scheme.vanishing_diam.map_continuous {β : Type u_1} {α : Type u_2} {A : list β set α} (hA : cantor_scheme.vanishing_diam A) :

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

theorem cantor_scheme.closure_antitone.map_of_vanishing_diam {β : Type u_1} {α : Type u_2} {A : list β set α} (hdiam : cantor_scheme.vanishing_diam A) (hanti : cantor_scheme.closure_antitone A) (hnonempty : (l : list β), (A l).nonempty) :

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