# 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.1, f x.2)) (uniformity β) =
structure UniformInducing {α : Type u} {β : Type v} [] [] (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.

• comap_uniformity : Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (uniformity β) =

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

Instances For
theorem UniformInducing.comap_uniformity {α : Type u} {β : Type v} [] [] {f : αβ} (self : ) :
Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (uniformity β) =

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

theorem uniformInducing_iff_uniformSpace {α : Type u} {β : Type v} [] [] {f : αβ} :
UniformSpace.comap f inst✝ = inst✝¹
theorem UniformInducing.comap_uniformSpace {α : Type u} {β : Type v} [] [] {f : αβ} :
UniformSpace.comap f inst✝ = inst✝¹

Alias of the forward direction of uniformInducing_iff_uniformSpace.

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 : (uniformity α).HasBasis p s) (h' : (uniformity β).HasBasis p' s') {f : αβ} :
(∀ (i : ι'), p' i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (j : ι), p j∃ (i : ι'), 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, ∀ (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.of_comp_iff {α : Type u} {β : Type v} {γ : Type w} [] [] [] {g : βγ} (hg : ) {f : αβ} :
theorem UniformInducing.basis_uniformity {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {ι : Sort u_1} {p : ιProp} {s : ιSet (β × β)} (H : (uniformity β).HasBasis p s) :
(uniformity α).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.uniformInducing_comp_iff {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {g : βγ} (hg : ) :
theorem UniformInducing.uniformContinuousOn_iff {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {g : βγ} {S : Set α} (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.1, e₂ p.2)
theorem UniformInducing.denseInducing {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (hd : ) :
theorem SeparationQuotient.uniformInducing_mk {α : Type u} [] :
UniformInducing SeparationQuotient.mk
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 :

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.

• comap_uniformity : Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (uniformity β) =
• inj :

A uniform embedding is injective.

Instances For
theorem UniformEmbedding.inj {α : Type u} {β : Type v} [] [] {f : αβ} (self : ) :

A uniform embedding is injective.

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 : (uniformity α).HasBasis p s) (h' : (uniformity β).HasBasis p' s') {f : αβ} :
(∀ (i : ι'), p' i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (j : ι), p j∃ (i : ι'), 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 : (uniformity α).HasBasis p s) (h' : (uniformity β).HasBasis p' s') {f : αβ} :
∀ (j : ι), p j∃ (i : ι'), 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 UniformEmbedding.of_comp_iff {α : Type u} {β : Type v} {γ : Type w} [] [] [] {g : βγ} (hg : ) {f : αβ} :
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.1, e₂ p.2)
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 isComplete_of_complete_image {α : Type u} {β : Type v} [] [] {m : αβ} {s : Set α} (hm : ) :
IsComplete (m '' s)

Alias of the forward direction of isComplete_image_iff.

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 : ) :
instance SeparationQuotient.instCompleteSpace {α : Type u} [] [] :
Equations
• =
theorem completeSpace_congr {α : Type u} {β : Type v} [] [] {e : α β} (he : ) :
theorem completeSpace_coe_iff_isComplete {α : Type u} [] {s : Set α} :
theorem IsComplete.completeSpace_coe {α : Type u} [] {s : Set α} :

Alias of the reverse direction of completeSpace_coe_iff_isComplete.

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.

Equations
• =
theorem completeSpace_extension {α : Type u} {β : Type v} [] [] {m : βα} (hm : ) (dense : ) (h : ∀ (f : ), ∃ (x : α), nhds x) :
theorem totallyBounded_image_iff {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} (hf : ) :
theorem totallyBounded_preimage {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set β} (hf : ) (hs : ) :
instance CompleteSpace.sum {α : Type u} {β : Type v} [] [] [] [] :
Equations
• =
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.

Equations
• = .replaceTopology
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 (Set.range e)) (hb : closure (e '' s) nhds b) (hs : ) (hp : xs, p 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 : α) :
Filter.Tendsto f (Filter.comap e (nhds a)) (nhds (.extend f a))
theorem uniformContinuous_uniformly_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} (h_f : ) [] :
UniformContinuous (.extend f)
theorem uniformly_extend_of_ind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : βα} (h_e : ) (h_dense : ) {f : βγ} (h_f : ) [] (b : β) :
.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 : ) :
.extend f = g