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 β] :
(α → β) → Prop

theorem uniform_inducing.mk' {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :
(∀ (s : set × α)), s 𝓤 α ∃ (t : set × β)) (H : t 𝓤 β), ∀ (x y : α), (f x, f y) t(x, y) s)uniform_inducing f

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 : α → β} :

structure uniform_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
(α → β) → 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 : α → β} :

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 : α → β} :

theorem uniform_inducing.uniform_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α → β} {g : β → γ} :

theorem uniform_inducing.inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {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₂ : β → β'} :
uniform_inducing e₁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 : α → β} :

theorem uniform_embedding.embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :

theorem uniform_embedding.dense_embedding {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :

theorem closure_image_mem_nhds_of_uniform_inducing {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set × α)} {e : α → β} (b : β) :
uniform_inducing edense_inducing es 𝓤 α(∃ (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 : α → β} :

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₂ : β → β'} :
uniform_embedding e₁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 α} :

theorem is_complete_image_iff {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : α → β} {s : set α} :

A set is complete iff its image under a uniform embedding is complete.

theorem complete_space_iff_is_complete_range {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :

theorem complete_space_congr {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {e : α β} :

theorem is_complete.complete_space_coe {α : Type u_1} [uniform_space α] {s : set α} :

theorem is_closed.complete_space_coe {α : Type u_1} [uniform_space α] [complete_space α] {s : set α} :

theorem complete_space_extension {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {m : β → α} :
uniform_inducing mdense_range m(∀ (f : filter β), cauchy f(∃ (x : α), filter.map m f 𝓝 x))complete_space α

theorem totally_bounded_preimage {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} {s : set β} :

theorem uniform_embedding_comap {α : Type u_1} {β : Type u_2} {f : α → β} [u : uniform_space β] :

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 α} :
uniform_continuous (λ (x : subtype p), f x.val)uniform_embedding e(∀ (x : β), x closure (set.range e))closure (e '' s) 𝓝 bis_closed s(∀ (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 : α → γ} :
(∀ (b : β), g (e b) = f b)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 γ] :