Cardinal control from a dense range

Every point of a metric space is determined by a sequence from any specified dense range. Besides its later cardinal consequences, the explicit embedding keeps the completion estimates independent of the internal representation of Mathlib's completion.

noncomputable def ScottishBook155.DenseSequenceCardinal.approx {D : Type u} {X : Type v} [MetricSpace X] (f : D → X) (hf : DenseRange f) (x : X) (n : ℕ) : D

A chosen 1 / (n+1) approximation from the dense source.

Equations

• ScottishBook155.DenseSequenceCardinal.approx f hf x n = Classical.choose ⋯

theorem ScottishBook155.DenseSequenceCardinal.approx_spec {D : Type u} {X : Type v} [MetricSpace X] (f : D → X) (hf : DenseRange f) (x : X) (n : ℕ) : dist (f (approx f hf x n)) x < 1 / (↑n + 1)

theorem ScottishBook155.DenseSequenceCardinal.approx_tendsto {D : Type u} {X : Type v} [MetricSpace X] (f : D → X) (hf : DenseRange f) (x : X) : Filter.Tendsto (fun (n : ℕ) => f (approx f hf x n)) Filter.atTop (nhds x)

noncomputable def ScottishBook155.DenseSequenceCardinal.sequenceEmbedding {D : Type u} {X : Type v} [MetricSpace X] (f : D → X) (hf : DenseRange f) : X ↪ ℕ → D

A metric space embeds into the type of sequences from any dense source.

Equations

• ScottishBook155.DenseSequenceCardinal.sequenceEmbedding f hf = { toFun := fun (x : X) => ScottishBook155.DenseSequenceCardinal.approx f hf x, inj' := ⋯ }

theorem ScottishBook155.DenseSequenceCardinal.mk_le_sequences {D : Type u} {X : Type v} [MetricSpace X] (f : D → X) (hf : DenseRange f) : Cardinal.lift.{u, v} (Cardinal.mk X) ≤ Cardinal.lift.{v, u} (Cardinal.mk (ℕ → D))

Cardinal form of sequenceEmbedding.