dense_inducing extension of uniform_continuous functions

Stream: Is there code for X?

[Xavier Roblot]

Do we have something along the lines of the following result

import topology.uniform_space.cauchy
import topology.uniform_space.separation
import topology.dense_embedding

variables {α :Type*} [topological_space α] [uniform_space α]
variables {β : Type*} [topological_space β] [uniform_space β]
variables {γ : Type*} [uniform_space γ] [complete_space γ] [separated_space γ]

lemma continuous_extend_of_uniform_continuous {e : α → β} {f : α → γ}
  (de : dense_inducing e) (h : uniform_continuous f) :
  uniform_continuous (de.extend f) := sorry

I am not sure these are the optimal hypotheses though. I would also be happy with a result that only proves that extension is continuous.

[Anatole Dedecker]

In your case I think you can only get continuity (this is docs#dense_inducing.continuous_extend). If you want uniform continuity, you need e to be a docs#uniform_inducing, in which case you can use docs#uniform_continuous_uniformly_extend

[Anatole Dedecker]

By the way, having both topological_space α and uniform_space α in your context is probably not doing what you want

[Anatole Dedecker]

Wait actually you can’t even apply docs#dense_inducing_continuous_extend in your context, because if you want to show that f has all the limits you want using completeness you already need e to be a uniform inducing (this is docs#uniformly_extend_exists), so you may as well use docs#uniform_continuous_uniformly_extend directly

[Xavier Roblot]

I see. What if I have metric_space instead? Can I get a stronger statement that is using only dense_inducing?

[Xavier Roblot]

I found a result that is more or less what I want, it is Theorem 6.21 in https://www.researchgate.net/publication/305196408_INTRODUCTION_TO_UNIFORM_SPACES

[Anatole Dedecker]

Well the subtlety is that for a dense subset of a uniform space, coe is not merely a docs#dense_inducing, it is a docs#uniform_inducing with dense range

[Anatole Dedecker]

Basically, your hypotheses correspond to "let $A$ be a dense subset of a uniform space $E$, with a uniform structure on $A$ which corresponds to the topology induced from $E$", whereas the right hypotheses are stronger, because you don't simply want the topology on $A$ to be the induced topology, you want the uniform structure on $A$ to be the induced uniform structure

[Xavier Roblot]

Ok. I understand. Thanks !

[Xavier Roblot]

I have been trying to prove the fact that the inclusion of a set into its closure is a uniform_inducing with dense_range but I am having a lot of difficulties proving this last fact. Say $A$ is a subset of a uniform space $E$, I can use docs#uniform_embedding_set_inclusion to prove that the inclusion $A \subseteq \bar{A}$ is uniform_inducing but I cannot find a way to prove that corresponding inclusion map is dense_range, say something like that

import topology.constructions

example {α : Type*} [topological_space α] (A : set α) :
  dense_range (set.inclusion (@subset_closure α _ A)) := sorry

Now I have a strong feeling that I am not stating things properly (and indeed the statement of this result looks pretty awful) and that's probably why I cannot get anywhere, but I cannot find the right way to state things.

[Anatole Dedecker]

docs#dense_embedding.subtype should help you, but arguably that's indeed not a very practical way of stating things. Could you give more context to un- #xy ?

[Xavier Roblot]

Here is my setting. I have a subset R of ℂ and an uniform continuous map f : R → ℂ and I want to construct the extension of f to the closure of R, so I am trying something like that

import topology.algebra.uniform_field
import analysis.complex.basic

example (R : set ℂ) (f : R → ℂ) (h : uniform_continuous f) :
  closure R → ℂ :=
begin
  have := uniform_embedding_set_inclusion (@subset_closure ℂ _ R),
  refine (this.dense_inducing _).extend f,
  sorry,  -- need to prove: dense_range (set.inclusion subset_closure)
end