Theorems · Theorem · general topology

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.

Defined in

Mathlib.Topology.MetricSpace.CantorScheme

Cited by

3 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext, Classical.choice