mathlib documentation

topology.uniform_space.uniform_embedding

Uniform embeddings of uniform spaces. #

Extension of uniform continuous functions.

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.mk' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (h : ∀ (s : set × α)), s 𝓤 α ∃ (t : set × β)) (H : t 𝓤 β), ∀ (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 : (𝓤 β).has_basis p s) :
(𝓤 α).has_basis p (λ (i : ι), prod.map f f ⁻¹' s i)
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 uniform_embedding_subtype_val {α : Type u_1} [uniform_space α] {p : α → Prop} :
theorem uniform_embedding_subtype_coe {α : Type u_1} [uniform_space α] {p : α → Prop} :
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 uniform_embedding_def {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :
uniform_embedding f function.injective f ∀ (s : set × α)), s 𝓤 α ∃ (t : set × β)) (H : t 𝓤 β), ∀ (x y : α), (f x, f y) t(x, y) s
theorem uniform_embedding_def' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :
uniform_embedding f function.injective f uniform_continuous f ∀ (s : set × α)), s 𝓤 α(∃ (t : set × β)) (H : t 𝓤 β), ∀ (x y : α), (f x, f y) t(x, y) s)
theorem uniform_embedding_inl {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
theorem uniform_embedding_inr {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
@[protected]
theorem uniform_inducing.uniform_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] [separated_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 𝓤 β) (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 𝓤 β) (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 α.

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) :
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) :
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 𝓤 β) (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 𝓤 α) :
∃ (a : α), closure (e '' {a' : α | (a, a') s}) 𝓝 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.complete_space_coe {α : Type u_1} [uniform_space α] {s : set α} (hs : is_complete 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 complete_space_iff_is_complete_range {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} (hf : uniform_inducing f) :
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) :
theorem is_closed.complete_space_coe {α : Type u_1} [uniform_space α] [complete_space α] {s : set α} (hs : is_closed s) :
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 𝓝 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 (𝓝 a)) (𝓝 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) 𝓝 b) (hs : is_closed s) (hp : ∀ (x : α), x sp x) :
∃ (c : γ), filter.tendsto f (filter.comap e (𝓝 b)) (𝓝 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