# Documentation

Mathlib.Topology.UniformSpace.UniformEmbedding

# Uniform embeddings of uniform spaces. #

Extension of uniform continuous functions.

### Uniform inducing maps #

theorem uniformInducing_iff {α : Type u} {β : Type v} [] [] (f : αβ) :
Filter.comap (fun x => (f x.fst, f x.snd)) () =
structure UniformInducing {α : Type u} {β : Type v} [] [] (f : αβ) :
• comap_uniformity : Filter.comap (fun x => (f x.fst, f x.snd)) () =

The uniformity filter on the domain is the pullback of the uniformity filter on the codomain under Prod.map f f.

A map f : α → β between uniform spaces is called uniform inducing if the uniformity filter on α is the pullback of the uniformity filter on β under Prod.map f f. If α is a separated space, then this implies that f is injective, hence it is a UniformEmbedding.

Instances For
theorem UniformInducing.comap_uniformSpace {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
UniformSpace.comap f inst✝ = inst✝¹
theorem uniformInducing_iff' {α : Type u} {β : Type v} [] [] {f : αβ} :
theorem Filter.HasBasis.uniformInducing_iff {α : Type u} {β : Type v} [] [] {ι : Sort u_1} {ι' : Sort u_2} {p : ιProp} {p' : ι'Prop} {s : ιSet (α × α)} {s' : ι'Set (β × β)} (h : ) (h' : Filter.HasBasis () p' s') {f : αβ} :
(∀ (i : ι'), p' ij, p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (j : ι), p ji, p' i ∀ (x y : α), (f x, f y) s' i(x, y) s j
theorem UniformInducing.mk' {α : Type u} {β : Type v} [] [] {f : αβ} (h : ∀ (s : Set (α × α)), s t, t ∀ (x y : α), (f x, f y) t(x, y) s) :
theorem uniformInducing_id {α : Type u} [] :
theorem UniformInducing.comp {α : Type u} {β : Type v} {γ : Type w} [] [] [] {g : βγ} (hg : ) {f : αβ} (hf : ) :
theorem UniformInducing.basis_uniformity {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {ι : Sort u_1} {p : ιProp} {s : ιSet (β × β)} (H : ) :
Filter.HasBasis () p fun i => Prod.map f f ⁻¹' s i
theorem UniformInducing.cauchy_map_iff {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {F : } :
theorem uniformInducing_of_compose {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {g : βγ} (hf : ) (hg : ) (hgf : UniformInducing (g f)) :
theorem UniformInducing.uniformContinuous {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
theorem UniformInducing.uniformContinuous_iff {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {g : βγ} (hg : ) :
theorem UniformInducing.inducing {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) :
theorem UniformInducing.prod {α : Type u} {β : Type v} [] [] {α' : Type u_1} {β' : Type u_2} [] [] {e₁ : αα'} {e₂ : ββ'} (h₁ : ) (h₂ : ) :
UniformInducing fun p => (e₁ p.fst, e₂ p.snd)
theorem UniformInducing.denseInducing {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (hd : ) :
theorem UniformInducing.injective {α : Type u} {β : Type v} [] [] [] {f : αβ} (h : ) :

### Uniform embeddings #

theorem uniformEmbedding_iff {α : Type u} {β : Type v} [] [] (f : αβ) :
structure UniformEmbedding {α : Type u} {β : Type v} [] [] (f : αβ) extends :
• comap_uniformity : Filter.comap (fun x => (f x.fst, f x.snd)) () =
• inj :

A uniform embedding is injective.

A map f : α → β between uniform spaces is a uniform embedding if it is uniform inducing and injective. If α is a separated space, then the latter assumption follows from the former.

Instances For
theorem uniformEmbedding_iff' {α : Type u} {β : Type v} [] [] {f : αβ} :
theorem Filter.HasBasis.uniformEmbedding_iff' {α : Type u} {β : Type v} [] [] {ι : Sort u_1} {ι' : Sort u_2} {p : ιProp} {p' : ι'Prop} {s : ιSet (α × α)} {s' : ι'Set (β × β)} (h : ) (h' : Filter.HasBasis () p' s') {f : αβ} :
(∀ (i : ι'), p' ij, p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (j : ι), p ji, p' i ∀ (x y : α), (f x, f y) s' i(x, y) s j
theorem Filter.HasBasis.uniformEmbedding_iff {α : Type u} {β : Type v} [] [] {ι : Sort u_1} {ι' : Sort u_2} {p : ιProp} {p' : ι'Prop} {s : ιSet (α × α)} {s' : ι'Set (β × β)} (h : ) (h' : Filter.HasBasis () p' s') {f : αβ} :
∀ (j : ι), p ji, p' i ∀ (x y : α), (f x, f y) s' i(x, y) s j
theorem uniformEmbedding_subtype_val {α : Type u} [] {p : αProp} :
UniformEmbedding Subtype.val
theorem uniformEmbedding_set_inclusion {α : Type u} [] {s : Set α} {t : Set α} (hst : s t) :
theorem UniformEmbedding.comp {α : Type u} {β : Type v} {γ : Type w} [] [] [] {g : βγ} (hg : ) {f : αβ} (hf : ) :
theorem Equiv.uniformEmbedding {α : Type u_1} {β : Type u_2} [] [] (f : α β) (h₁ : ) (h₂ : UniformContinuous f.symm) :
theorem uniformEmbedding_inl {α : Type u} {β : Type v} [] [] :
theorem uniformEmbedding_inr {α : Type u} {β : Type v} [] [] :
theorem UniformInducing.uniformEmbedding {α : Type u} {β : Type v} [] [] [] {f : αβ} (hf : ) :

If the domain of a UniformInducing map f is a T₀ space, then f is injective, hence it is a UniformEmbedding.

theorem uniformEmbedding_iff_uniformInducing {α : Type u} {β : Type v} [] [] [] {f : αβ} :
theorem comap_uniformity_of_spaced_out {β : Type v} [] {α : Type u_1} {f : αβ} {s : Set (β × β)} (hs : s ) (hf : Pairwise fun x y => ¬(f x, f y) s) :

If a map f : α → β sends any two distinct points to point that are not related by a fixed s ∈ 𝓤 β, then f is uniform inducing with respect to the discrete uniformity on α: the preimage of 𝓤 β under prod.map f f is the principal filter generated by the diagonal in α × α.

theorem uniformEmbedding_of_spaced_out {β : Type v} [] {α : Type u_1} {f : αβ} {s : Set (β × β)} (hs : s ) (hf : Pairwise fun x y => ¬(f x, f y) s) :

If a map f : α → β sends any two distinct points to point that are not related by a fixed s ∈ 𝓤 β, then f is a uniform embedding with respect to the discrete uniformity on α.

theorem UniformEmbedding.embedding {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) :
theorem UniformEmbedding.denseEmbedding {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (hd : ) :
theorem closedEmbedding_of_spaced_out {β : Type v} [] {α : Type u_1} [] [] [] {f : αβ} {s : Set (β × β)} (hs : s ) (hf : Pairwise fun x y => ¬(f x, f y) s) :
theorem closure_image_mem_nhds_of_uniformInducing {α : Type u} {β : Type v} [] [] {s : Set (α × α)} {e : αβ} (b : β) (he₁ : ) (he₂ : ) (hs : s ) :
a, closure (e '' {a' | (a, a') s}) nhds b
theorem uniformEmbedding_subtypeEmb {α : Type u} {β : Type v} [] [] (p : αProp) {e : αβ} (ue : ) (de : ) :
theorem UniformEmbedding.prod {α : Type u} {β : Type v} [] [] {α' : Type u_1} {β' : Type u_2} [] [] {e₁ : αα'} {e₂ : ββ'} (h₁ : ) (h₂ : ) :
UniformEmbedding fun p => (e₁ p.fst, e₂ p.snd)
theorem isComplete_of_complete_image {α : Type u} {β : Type v} [] [] {m : αβ} {s : Set α} (hm : ) (hs : IsComplete (m '' s)) :
theorem IsComplete.completeSpace_coe {α : Type u} [] {s : Set α} (hs : ) :
theorem isComplete_image_iff {α : Type u} {β : Type v} [] [] {m : αβ} {s : Set α} (hm : ) :

A set is complete iff its image under a uniform inducing map is complete.

theorem completeSpace_iff_isComplete_range {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
theorem UniformInducing.isComplete_range {α : Type u} {β : Type v} [] [] [] {f : αβ} (hf : ) :
theorem completeSpace_congr {α : Type u} {β : Type v} [] [] {e : α β} (he : ) :
theorem completeSpace_coe_iff_isComplete {α : Type u} [] {s : Set α} :
theorem IsClosed.completeSpace_coe {α : Type u} [] [] {s : Set α} (hs : ) :
instance ULift.completeSpace {α : Type u} [] [h : ] :

The lift of a complete space to another universe is still complete.

theorem completeSpace_extension {α : Type u} {β : Type v} [] [] {m : βα} (hm : ) (dense : ) (h : ∀ (f : ), x, nhds x) :
theorem totallyBounded_preimage {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set β} (hf : ) (hs : ) :
instance CompleteSpace.sum {α : Type u} {β : Type v} [] [] [] [] :
theorem uniformEmbedding_comap {α : Type u_1} {β : Type u_2} {f : αβ} [u : ] (hf : ) :
def Embedding.comapUniformSpace {α : Type u_1} {β : Type u_2} [] [u : ] (f : αβ) (h : ) :

Pull back a uniform space structure by an embedding, adjusting the new uniform structure to make sure that its topology is defeq to the original one.

Instances For
theorem Embedding.to_uniformEmbedding {α : Type u_1} {β : Type u_2} [] [u : ] (f : αβ) (h : ) :
theorem uniformly_extend_exists {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} (h_f : ) [] (a : α) :
c, Filter.Tendsto f (Filter.comap e (nhds a)) (nhds c)
theorem uniform_extend_subtype {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {p : αProp} {e : αβ} {f : αγ} {b : β} {s : Set α} (hf : UniformContinuous fun x => f x) (he : ) (hd : ∀ (x : β), x closure ()) (hb : closure (e '' s) nhds b) (hs : ) (hp : (x : α) → x sp x) :
c, Filter.Tendsto f (Filter.comap e (nhds b)) (nhds c)
theorem uniformly_extend_spec {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} (h_f : ) [] (a : α) :
theorem uniformContinuous_uniformly_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} (h_f : ) [] :
theorem uniformly_extend_of_ind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} (h_f : ) [] (b : β) :
DenseInducing.extend (_ : ) f (e b) = f b
theorem uniformly_extend_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} [] {g : αγ} (hg : ∀ (b : β), g (e b) = f b) (hc : ) :