mathlib3 documentation

topology.uniform_space.uniform_embedding

Uniform embeddings of uniform spaces. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Extension of uniform continuous functions.

Uniform inducing maps #

structure uniform_inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α β) :
Prop

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 uniform_embedding.

theorem uniform_inducing_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α β) :
uniform_inducing f filter.comap (λ (x : α × α), (f x.fst, f x.snd)) (uniformity β) = uniformity α
@[protected]
theorem uniform_inducing.comap_uniform_space {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (hf : uniform_inducing f) :
uniform_space.comap f _inst_2 = _inst_1
@[protected]
theorem filter.has_basis.uniform_inducing_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {ι : Sort u_3} {ι' : Sort u_4} {p : ι Prop} {p' : ι' Prop} {s : ι set × α)} {s' : ι' set × β)} (h : (uniformity α).has_basis p s) (h' : (uniformity β).has_basis p' s') {f : α β} :
uniform_inducing 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 uniform_inducing.mk' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (h : (s : set × α)), s uniformity α (t : set × β)) (H : t uniformity β), (x y : α), (f x, f y) t (x, y) s) :
theorem uniform_inducing.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {g : β γ} (hg : uniform_inducing g) {f : α β} (hf : uniform_inducing f) :
theorem uniform_inducing.basis_uniformity {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (hf : uniform_inducing f) {ι : Sort u_3} {p : ι Prop} {s : ι set × β)} (H : (uniformity β).has_basis p s) :
(uniformity α).has_basis p (λ (i : ι), prod.map f f ⁻¹' s i)
theorem uniform_inducing.cauchy_map_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (hf : uniform_inducing f) {F : filter α} :
theorem uniform_inducing_of_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α β} {g : β γ} (hf : uniform_continuous f) (hg : uniform_continuous g) (hgf : uniform_inducing (g f)) :
theorem uniform_inducing.uniform_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (hf : uniform_inducing f) :
theorem uniform_inducing.uniform_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α β} {g : β γ} (hg : uniform_inducing g) :
@[protected]
theorem uniform_inducing.inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (h : uniform_inducing f) :
theorem uniform_inducing.prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {α' : Type u_3} {β' : Type u_4} [uniform_space α'] [uniform_space β'] {e₁ : α α'} {e₂ : β β'} (h₁ : uniform_inducing e₁) (h₂ : uniform_inducing e₂) :
uniform_inducing (λ (p : α × β), (e₁ p.fst, e₂ p.snd))
theorem uniform_inducing.dense_inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (h : uniform_inducing f) (hd : dense_range f) :
@[protected]
theorem uniform_inducing.injective {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] [t0_space α] {f : α β} (h : uniform_inducing f) :
structure uniform_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α β) :
Prop

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.

theorem filter.has_basis.uniform_embedding_iff' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {ι : Sort u_3} {ι' : Sort u_4} {p : ι Prop} {p' : ι' Prop} {s : ι set × α)} {s' : ι' set × β)} (h : (uniformity α).has_basis p s) (h' : (uniformity β).has_basis p' s') {f : α β} :
uniform_embedding f function.injective 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.has_basis.uniform_embedding_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {ι : Sort u_3} {ι' : Sort u_4} {p : ι Prop} {p' : ι' Prop} {s : ι set × α)} {s' : ι' set × β)} (h : (uniformity α).has_basis p s) (h' : (uniformity β).has_basis p' s') {f : α β} :
uniform_embedding f function.injective f uniform_continuous f (j : ι), p j ( (i : ι'), p' i (x y : α), (f x, f y) s' i (x, y) s j)
theorem uniform_embedding_set_inclusion {α : Type u_1} [uniform_space α] {s t : set α} (hst : s t) :
theorem uniform_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {g : β γ} (hg : uniform_embedding g) {f : α β} (hf : uniform_embedding f) :
theorem equiv.uniform_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α β) (h₁ : uniform_continuous f) (h₂ : uniform_continuous (f.symm)) :
@[protected]
theorem uniform_inducing.uniform_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] [t0_space α] {f : α β} (hf : uniform_inducing f) :

If the domain of a uniform_inducing map f is a separated_space, then f is injective, hence it is a uniform_embedding.

theorem comap_uniformity_of_spaced_out {β : Type u_2} [uniform_space β] {α : Type u_1} {f : α β} {s : set × β)} (hs : s uniformity β) (hf : pairwise (λ (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 uniform_embedding_of_spaced_out {β : Type u_2} [uniform_space β] {α : Type u_1} {f : α β} {s : set × β)} (hs : s uniformity β) (hf : pairwise (λ (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 α.

@[protected]
theorem uniform_embedding.embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (h : uniform_embedding f) :
theorem uniform_embedding.dense_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (h : uniform_embedding f) (hd : dense_range f) :
theorem closed_embedding_of_spaced_out {β : Type u_2} [uniform_space β] {α : Type u_1} [topological_space α] [discrete_topology α] [separated_space β] {f : α β} {s : set × β)} (hs : s uniformity β) (hf : pairwise (λ (x y : α), (f x, f y) s)) :
theorem closure_image_mem_nhds_of_uniform_inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set × α)} {e : α β} (b : β) (he₁ : uniform_inducing e) (he₂ : dense_inducing e) (hs : s uniformity α) :
(a : α), closure (e '' {a' : α | (a, a') s}) nhds b
theorem uniform_embedding_subtype_emb {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (p : α Prop) {e : α β} (ue : uniform_embedding e) (de : dense_embedding e) :
theorem uniform_embedding.prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {α' : Type u_3} {β' : Type u_4} [uniform_space α'] [uniform_space β'] {e₁ : α α'} {e₂ : β β'} (h₁ : uniform_embedding e₁) (h₂ : uniform_embedding e₂) :
uniform_embedding (λ (p : α × β), (e₁ p.fst, e₂ p.snd))
theorem is_complete_of_complete_image {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : α β} {s : set α} (hm : uniform_inducing m) (hs : is_complete (m '' s)) :
theorem is_complete_image_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : α β} {s : set α} (hm : uniform_inducing m) :

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

theorem uniform_inducing.is_complete_range {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] [complete_space α] {f : α β} (hf : uniform_inducing f) :
theorem complete_space_congr {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {e : α β} (he : uniform_embedding e) :
@[protected, instance]

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

theorem complete_space_extension {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : β α} (hm : uniform_inducing m) (dense : dense_range m) (h : (f : filter β), cauchy f ( (x : α), filter.map m f nhds x)) :
theorem totally_bounded_preimage {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} {s : set β} (hf : uniform_embedding f) (hs : totally_bounded s) :
@[protected, instance]
def complete_space.sum {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] [complete_space α] [complete_space β] :
theorem uniform_embedding_comap {α : Type u_1} {β : Type u_2} {f : α β} [u : uniform_space β] (hf : function.injective f) :
def embedding.comap_uniform_space {α : Type u_1} {β : Type u_2} [topological_space α] [u : uniform_space β] (f : α β) (h : embedding f) :

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
theorem embedding.to_uniform_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [u : uniform_space β] (f : α β) (h : embedding f) :
theorem uniformly_extend_exists {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β γ} (h_f : uniform_continuous f) [complete_space γ] (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} [uniform_space α] [uniform_space β] [uniform_space γ] [complete_space γ] {p : α Prop} {e : α β} {f : α γ} {b : β} {s : set α} (hf : uniform_continuous (λ (x : subtype p), f x.val)) (he : uniform_embedding e) (hd : (x : β), x closure (set.range e)) (hb : closure (e '' s) nhds b) (hs : is_closed s) (hp : (x : α), x s 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} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β γ} (h_f : uniform_continuous f) [complete_space γ] (a : α) :
theorem uniform_continuous_uniformly_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β γ} (h_f : uniform_continuous f) [cγ : complete_space γ] :
theorem uniformly_extend_of_ind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β γ} (h_f : uniform_continuous f) [separated_space γ] (b : β) :
_.extend f (e b) = f b
theorem uniformly_extend_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {e : β α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β γ} [separated_space γ] {g : α γ} (hg : (b : β), g (e b) = f b) (hc : continuous g) :
_.extend f = g