Theorems · Definition · general topology

CantorScheme.inducedMap

{β : Type u_1} → {α : Type u_2} → (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.

Defined in

Mathlib.Topology.MetricSpace.CantorScheme

Cited by

5 results in Mathlib

Foundations

Depth 9 from the axioms · uses Classical.choice