Documentation

Mathlib.Topology.MetricSpace.CantorScheme

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

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 #

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
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 α) [TopologicalSpace α] :

      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 : (CantorScheme.inducedMap A).fst) (n : ) :
          (CantorScheme.inducedMap A).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.Antitone.closureAntitone {β : Type u_1} {α : Type u_2} {A : List βSet α} [TopologicalSpace α] (hanti : CantorScheme.Antitone A) (hclosed : ∀ (l : List β), IsClosed (A l)) :

          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 α) [PseudoMetricSpace α] :

          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 α} [PseudoMetricSpace α] (hA : CantorScheme.VanishingDiam A) (ε : ) (ε_pos : 0 < ε) (x : β) :
            ∃ (n : ), yA (PiNat.res x n), zA (PiNat.res x n), dist y z < ε

            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 α} [PseudoMetricSpace α] [CompleteSpace α] (hdiam : CantorScheme.VanishingDiam A) (hanti : CantorScheme.ClosureAntitone A) (hnonempty : ∀ (l : List β), (A l).Nonempty) :
            (CantorScheme.inducedMap A).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.