CantorScheme.Disjoint.map_injective
theorem CantorScheme.Disjoint.map_injective :
∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α},
CantorScheme.Disjoint A → Function.Injective (CantorScheme.inducedMap A).snd
This theorem states that if we have a scheme, where the children of each set are pairwise disjoint, then the map induced by this scheme is injective. In other words, given any types `β` and `α`, and a function `A` from lists of `β` to sets of `α`, if the sets produced by `A` for each list are pairwise disjoint, then for any two different inputs to the map induced by `A`, the outputs will also be different.
More concisely: If `A` is a function from lists of type `β` to pairwise disjoint sets of type `α`, then `A` induces an injective map.
|
CantorScheme.map_mem
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)
The theorem `CantorScheme.map_mem` asserts that for any given type `β` and `α`, and a given scheme `A` which is a function from list of `β` to a set of `α`, if a sequence `x` lies in the domain of the map induced by `A` (as defined by `CantorScheme.inducedMap A`), then the image of `x` under this map is a member of each set `A` along the corresponding branch, where the branch is determined by the restriction of the sequence `x` to `n` (as defined by `PiNat.res`). In other words, the map produced by a Cantor scheme sends each sequence in its domain to an element that inhabits each set along the path described by that sequence.
More concisely: For any Cantor scheme `A` from a type `β` to a set of `α`, if a sequence `x` is in the domain of `A`'s induced map and `n` is a natural number, then the image of `x` under `A`'s map is in the set `A` at position `n` determined by the restriction of `x` to the first `n` elements.
|
CantorScheme.ClosureAntitone.map_of_vanishingDiam
theorem CantorScheme.ClosureAntitone.map_of_vanishingDiam :
∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : PseudoMetricSpace α] [inst_1 : CompleteSpace α],
CantorScheme.VanishingDiam A →
CantorScheme.ClosureAntitone A →
(∀ (l : List β), (A l).Nonempty) → (CantorScheme.inducedMap A).fst = Set.univ
This theorem states that for any scheme `A` on a complete space of type `α` (with `α` being a pseudo metric space), if the scheme has a vanishing diameter and each set in the scheme contains the closure of its children, then the map induced by the scheme is total. That is, for every list `l` of type `β`, the set `A l` is nonempty, and the first element of the pair produced by the induced map of `A` is the universal set. In other words, the induced map covers all elements in the space `α`.
More concisely: If `A` is a scheme on a complete pseudo metric space `α` with vanishing diameter and such that each set in `A` contains the closure of its children, then the induced map of `A` is total, i.e., for every list `l` of type `β`, the set `Al` is nonempty.
|
CantorScheme.VanishingDiam.map_continuous
theorem CantorScheme.VanishingDiam.map_continuous :
∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : DiscreteTopology β], CantorScheme.VanishingDiam A → Continuous (CantorScheme.inducedMap A).snd
This theorem states that for any two types `β` and `α`, and a `β`-scheme `A` on `α`, given that `α` is a PseudoMetricSpace and `β` is a TopologicalSpace with DiscreteTopology, if the `β`-scheme `A` has vanishing diameter along each branch, then the map induced by the `β`-scheme `A` is continuous. In other words, in the context of a scheme on a metric space which has vanishing diameter (meaning that the diameter approaches 0 along each branch), there exists a continuous map, which is induced by the scheme, from infinite sequences to elements in the intersection along the branch corresponding to each sequence.
More concisely: If `β` is a DiscreteTopology over a Type `β`, `α` is a MetricSpace, and `A` is a `β`-scheme on `α` with vanishing diameter along each branch, then `A` induces a continuous map from infinite sequences in `α` to their intersection along each branch.
|