Completion and recovery lemmas for coherent limit stages

The limit-stage proof uses common finite-coordinate truncations. Abstractly, these give simultaneous approximants whose mutual distance never exceeds the limit distance. This file isolates the two consequences needed later: short-distance preservation passes to the completion, and a jointly separating family of recovered coordinates forces injectivity.

def ScottishBook155.HasDistanceControlledApproximants (E : Type u) [PseudoMetricSpace E] : Prop

Simultaneous sequential approximants in a dense metric subspace, with no increase of the distance between the two approximated points.

Equations

• One or more equations did not get rendered due to their size.

def ScottishBook155.HasDistanceControlledNetApproximants (E : Type u) [PseudoMetricSpace E] (A : Type w) (l : Filter A) : Prop

Simultaneous approximants indexed by an arbitrary nontrivial filter. This is the form naturally supplied by finite-coordinate truncations ordered by inclusion.

Equations

• One or more equations did not get rendered due to their size.

theorem ScottishBook155.completionExtension_preservesUpTo_of_net {E : Type u} {F : Type v} {A : Type w} [PseudoMetricSpace E] [MetricSpace F] [CompleteSpace F] {l : Filter A} [l.NeBot] {f : E → F} {r : ℝ} (hf : LipschitzWith 1 f) (hshort : PreservesUpTo r f) (happrox : HasDistanceControlledNetApproximants E A l) : PreservesUpTo r (UniformSpace.Completion.extension f)

Exact preservation below a fixed scale passes to the completion from a common distance-controlled approximating net.

theorem ScottishBook155.completionExtension_preservesUpTo {E : Type u} {F : Type v} [PseudoMetricSpace E] [MetricSpace F] [CompleteSpace F] {f : E → F} {r : ℝ} (hf : LipschitzWith 1 f) (hshort : PreservesUpTo r f) (happrox : HasDistanceControlledApproximants E) : PreservesUpTo r (UniformSpace.Completion.extension f)

Exact preservation below a fixed scale passes to the completion whenever the dense subspace has common distance-controlled approximants.

theorem ScottishBook155.injective_of_jointlySeparating_recovery {X : Type u} {Y : Type v} {ι : Type w} {Z : ι → Type u_1} (f : X → Y) (project : (i : ι) → X → Z i) (recover : (i : ι) → Y → Z i) (hrecover : ∀ (i : ι) (x : X), recover i (f x) = project i x) (hseparate : ∀ (x y : X), (∀ (i : ι), project i x = project i y) → x = y) : Function.Injective f

Coordinate recovery proves injectivity whenever the recovered coordinates jointly separate the source.

theorem ScottishBook155.injective_of_eventuallySeparating_recovery {X : Type u} {Y : Type v} {A : Type w} {Z : A → Type u_1} {l : Filter A} (f : X → Y) (project : (i : A) → X → Z i) (recover : (i : A) → Y → Z i) (hrecover : ∀ (x : X), ∀ᶠ (i : A) in l, recover i (f x) = project i x) (hseparate : ∀ (x y : X), (∀ᶠ (i : A) in l, project i x = project i y) → x = y) : Function.Injective f

Eventual coordinate recovery is enough for injectivity when eventual equality of the recovered prefixes separates source points. This is the form used after all coordinates larger than the flat recovery band have appeared.

theorem ScottishBook155.eq_of_eventually_eq_of_tendsto {X : Type u} [TopologicalSpace X] [T2Space X] {A : Type v} {l : Filter A} [l.NeBot] (project : A → X → X) (hproject : ∀ (x : X), Filter.Tendsto (fun (i : A) => project i x) l (nhds x)) {x y : X} (hxy : ∀ᶠ (i : A) in l, project i x = project i y) : x = y

Eventual equality of approximating projections implies equality of their limits.

theorem ScottishBook155.injective_of_eventual_stage_recovery {X : Type u} [TopologicalSpace X] [T2Space X] {Y : Type v} {A : Type w} {l : Filter A} [l.NeBot] {Xstage : A → Type u_1} {Ystage : A → Type u_2} (f : X → Y) (stageMap : (i : A) → Xstage i → Ystage i) (stageInjective : ∀ (i : A), Function.Injective (stageMap i)) (project : (i : A) → X → Xstage i) (embed : (i : A) → Xstage i → X) (recover : (i : A) → Y → Ystage i) (hproject : ∀ (x : X), Filter.Tendsto (fun (i : A) => embed i (project i x)) l (nhds x)) (hrecover : ∀ (x : X), ∀ᶠ (i : A) in l, recover i (f x) = stageMap i (project i x)) : Function.Injective f

A completed limit map is injective when its coherent retractions eventually recover injective earlier-stage maps and the source projections converge to the identity.