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
- comap_uniformity : filter.comap (λ (x : α × α), (f x.fst, f x.snd)) (uniformity β) = uniformity α
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
theorem
uniform_inducing_iff'
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β} :
uniform_inducing f ↔ uniform_continuous f ∧ filter.comap (prod.map f f) (uniformity β) ≤ uniformity α
@[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 : α → β} :
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) :
uniform_inducing (g ∘ 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 α} :
cauchy (filter.map f F) ↔ cauchy F
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) :
uniform_continuous f ↔ uniform_continuous (g ∘ f)
@[protected]
theorem
uniform_inducing.inducing
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β}
(h : 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₂ : β → β'}
(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
- to_uniform_inducing : uniform_inducing f
- inj : function.injective f
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_iff
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
(f : α → β) :
theorem
uniform_embedding_iff'
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
{f : α → β} :
uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ filter.comap (prod.map f f) (uniformity β) ≤ uniformity α
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 : α → β} :
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) :
uniform_embedding (g ∘ 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
uniform_embedding_iff_uniform_inducing
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
[t0_space α]
{f : α → β} :
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)) :
filter.comap (prod.map f f) (uniformity β) = filter.principal id_rel
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 α) :
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) :
is_complete (m '' s) ↔ is_complete s
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) :
complete_space α ↔ is_complete (set.range f)
theorem
uniform_inducing.is_complete_range
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
[complete_space α]
{f : α → β}
(hf : uniform_inducing f) :
is_complete (set.range 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) :
@[protected, instance]
def
ulift.complete_space
{α : Type u_1}
[uniform_space α]
[h : complete_space α] :
complete_space (ulift α)
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) :
totally_bounded (f ⁻¹' s)
@[protected, instance]
def
complete_space.sum
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
[complete_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 : α) :
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)
[cγ : complete_space γ] :
uniform_continuous (_.extend f)
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 : α → γ}
(hg : ∀ (b : β), g (e b) = f b)
(hc : continuous g) :