Paths in uniform spaces

In this file we define a UniformSpace structure on Paths between two points in a uniform space and prove that various functions associated with Paths are uniformly continuous.

The uniform space structure is induced from the space of continuous maps C(I, X), and corresponds to uniform convergence of paths on I, see Path.hasBasis_uniformity.

instance Path.instUniformSpace {X : Type u_1} [UniformSpace X] {x y : X} : UniformSpace (Path x y)

Equations

• Path.instUniformSpace = UniformSpace.comap toContinuousMap ContinuousMap.compactConvergenceUniformSpace

theorem Path.isUniformEmbedding_coe {X : Type u_1} [UniformSpace X] {x y : X} : IsUniformEmbedding _root_.toContinuousMap

theorem Path.uniformContinuous {X : Type u_1} [UniformSpace X] {x y : X} (γ : Path x y) : UniformContinuous ⇑γ

theorem Path.uniformContinuous_extend {X : Type u_1} [UniformSpace X] {x y : X} (γ : Path x y) : UniformContinuous ⇑γ.extend

Given a path γ, it extension to the real line γ.extend : C(ℝ, X) is a uniformly continuous function.

theorem Path.uniformContinuous_extend_left {X : Type u_1} [UniformSpace X] {x y : X} : UniformContinuous extend

The function sending a path γ to its extension γ.extend : ℝ → X is uniformly continuous in γ.

theorem Filter.HasBasis.uniformityPath {X : Type u_1} [UniformSpace X] {x y : X} {ι : Sort u_2} {p : ι → Prop} {U : ι → Set (X × X)} (hU : (uniformity X).HasBasis p U) : (uniformity (Path x y)).HasBasis p fun (i : ι) => {γ : Path x y × Path x y | ∀ (t : ↑unitInterval), (γ.1 t, γ.2 t) ∈ U i}

If {U i | p i} form a basis of entourages of X, then the entourages {V i | p i}, V i = {(γ₁, γ₂) | ∀ t, (γ₁ t, γ₂ t) ∈ U i}, form a basis of entourages of paths between x and y.

theorem Path.hasBasis_uniformity {X : Type u_1} [UniformSpace X] {x y : X} : (uniformity (Path x y)).HasBasis (fun (x : Set (X × X)) => x ∈ uniformity X) fun (x_1 : Set (X × X)) => {γ : Path x y × Path x y | ∀ (t : ↑unitInterval), (γ.1 t, γ.2 t) ∈ x_1}

theorem Path.uniformContinuous_symm {X : Type u_1} [UniformSpace X] {x y : X} : UniformContinuous symm

theorem Path.uniformContinuous_trans {X : Type u_1} [UniformSpace X] {x y z : X} : UniformContinuous (Function.uncurry trans)

The function Path.trans that concatenates two paths γ₁ : Path x y and γ₂ : Path y z is uniformly continuous in (γ₁, γ₂).

instance Path.instCompleteSpace {X : Type u_1} [UniformSpace X] {x y : X} [CompleteSpace X] : CompleteSpace (Path x y)

The space of paths between two points in a complete uniform space is a complete uniform space.