Uniform embeddings of uniform spaces.
Extension of uniform continuous functions.
structure
uniform_inducing
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β] :
(α → β) → Prop
- comap_uniformity : filter.comap (λ (x : α × α), (f x.fst, f x.snd)) (uniformity β) = uniformity α
theorem
uniform_inducing.mk'
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β} :
(∀ (s : set (α × α)), s ∈ uniformity α ↔ ∃ (t : set (β × β)) (H : t ∈ uniformity β), ∀ (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 : α → β} :
uniform_inducing f → uniform_inducing (g ∘ f)
structure
uniform_embedding
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β] :
(α → β) → Prop
- to_uniform_inducing : uniform_inducing f
- inj : function.injective f
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 : α → β} :
uniform_embedding f → 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 ∈ uniformity α ↔ ∃ (t : set (β × β)) (H : t ∈ uniformity β), ∀ (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 ∈ uniformity α → (∃ (t : set (β × β)) (H : t ∈ uniformity β), ∀ (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 : β → γ} :
uniform_inducing g → (uniform_continuous f ↔ uniform_continuous (g ∘ f))
theorem
uniform_inducing.inducing
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β} :
uniform_inducing f → 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₂ : β → β'} :
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 : α → β} :
uniform_inducing f → dense_range f → dense_inducing f
theorem
uniform_embedding.embedding
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β} :
uniform_embedding f → embedding f
theorem
uniform_embedding.dense_embedding
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β} :
uniform_embedding f → dense_range f → dense_embedding 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 e → dense_inducing e → 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 : α → β} :
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 α} :
uniform_inducing m → is_complete (m '' s) → is_complete s
theorem
is_complete_image_iff
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{m : α → β}
{s : set α} :
uniform_embedding m → (is_complete (m '' s) ↔ is_complete s)
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 : α → β} :
uniform_embedding f → (complete_space α ↔ is_complete (set.range f))
theorem
complete_space_congr
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{e : α ≃ β} :
uniform_embedding ⇑e → (complete_space α ↔ complete_space β)
theorem
is_complete.complete_space_coe
{α : Type u_1}
[uniform_space α]
{s : set α} :
is_complete s → complete_space ↥s
theorem
is_closed.complete_space_coe
{α : Type u_1}
[uniform_space α]
[complete_space α]
{s : set α} :
is_closed s → complete_space ↥s
theorem
complete_space_extension
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{m : β → α} :
uniform_inducing m → dense_range m → (∀ (f : filter β), cauchy f → (∃ (x : α), filter.map m f ≤ nhds x)) → complete_space α
theorem
totally_bounded_preimage
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β}
{s : set β} :
uniform_embedding f → totally_bounded s → totally_bounded (f ⁻¹' s)
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 α} :
uniform_continuous (λ (x : subtype p), f x.val) → uniform_embedding e → (∀ (x : β), x ∈ closure (set.range e)) → closure (e '' s) ∈ nhds b → is_closed s → (∀ (x : α), x ∈ s → p x) → (∃ (c : γ), filter.tendsto f (filter.comap e (nhds b)) (nhds 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 : β) :
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 : α) :
filter.tendsto f (filter.comap e (nhds a)) (nhds (_.extend f 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 γ] :
uniform_continuous (_.extend f)