mathlib3 documentation

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 #

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.

References #

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 α) [topological_space α] :
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 : ((cantor_scheme.induced_map A).fst)) (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.antitone.closure_antitone {β : Type u_1} {α : Type u_2} {A : list β set α} [topological_space α] (hanti : cantor_scheme.antitone A) (hclosed : (l : list β), is_closed (A l)) :

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 α) [pseudo_metric_space α] :
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 α} [pseudo_metric_space α] (hA : cantor_scheme.vanishing_diam A) (ε : ) (ε_pos : 0 < ε) (x : β) :
(n : ), (y : α), y A (pi_nat.res x n) (z : α), z A (pi_nat.res x n) has_dist.dist y z < ε

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.