Theorems · Definition · general topology

Metric.PiNatEmbed.distDenseSeq

(X : Type u_3) → [inst : MetricSpace X] → [TopologicalSpace.SeparableSpace X] → ℕ → X → ↑unitInterval

Given a separable metric space X, denseSeq X : ℕ → X gives a countable dense sequence. This measures the distance between denseSeq X n and x, truncated to the unit interval I so that the distances remain bounded. The function (fun x n ↦ distDenseSeq n x) : X → ℕ → I is a mapping from X to the Hilbert cube.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

6 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpaceTopologicalSpace.SeparableSpace