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
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) :
structure uniform_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α → β) :
Prop
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_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 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) :
theorem uniform_embedding_comap {α : Type u_1} {β : Type u_2} {f : α → β} [u : uniform_space β] (hf : function.injective 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_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
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) [separated_space γ] [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) [separated_space γ] [cγ : complete_space γ] :