Uniform embeddings of uniform spaces. #
Extension of uniform continuous functions.
Uniform inducing maps #
theorem
uniformInducing_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
:
UniformInducing f ↔ Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (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 UniformEmbedding.
- comap_uniformity : Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (uniformity β) = uniformity α
The uniformity filter on the domain is the pullback of the uniformity filter on the codomain under
Prod.map f f.
Instances For
theorem
uniformInducing_iff_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
UniformInducing f ↔ UniformSpace.comap f inst✝ = inst✝¹
theorem
UniformInducing.comap_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
UniformInducing f → UniformSpace.comap f inst✝ = inst✝¹
Alias of the forward direction of uniformInducing_iff_uniformSpace.
theorem
uniformInducing_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
UniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
theorem
Filter.HasBasis.uniformInducing_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : Filter.HasBasis (uniformity α) p s)
(h' : Filter.HasBasis (uniformity β) p' s')
{f : α → β}
:
theorem
UniformInducing.mk'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : ∀ (s : Set (α × α)), s ∈ uniformity α ↔ ∃ t ∈ uniformity β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s)
:
theorem
UniformInducing.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : UniformInducing g)
{f : α → β}
(hf : UniformInducing f)
:
UniformInducing (g ∘ f)
theorem
UniformInducing.basis_uniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
{ι : Sort u_1}
{p : ι → Prop}
{s : ι → Set (β × β)}
(H : Filter.HasBasis (uniformity β) p s)
:
Filter.HasBasis (uniformity α) p fun (i : ι) => Prod.map f f ⁻¹' s i
theorem
UniformInducing.cauchy_map_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
{F : Filter α}
:
Cauchy (Filter.map f F) ↔ Cauchy F
theorem
uniformInducing_of_compose
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
(hgf : UniformInducing (g ∘ f))
:
theorem
UniformInducing.uniformContinuous
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
:
theorem
UniformInducing.uniformContinuous_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : UniformInducing g)
:
UniformContinuous f ↔ UniformContinuous (g ∘ f)
theorem
UniformInducing.uniformContinuousOn_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
{S : Set α}
(hg : UniformInducing g)
:
UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S
theorem
UniformInducing.inducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : UniformInducing f)
:
Inducing f
theorem
UniformInducing.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : UniformInducing e₁)
(h₂ : UniformInducing e₂)
:
UniformInducing fun (p : α × β) => (e₁ p.1, e₂ p.2)
theorem
UniformInducing.denseInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : UniformInducing f)
(hd : DenseRange f)
:
theorem
UniformInducing.injective
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(h : UniformInducing f)
:
Uniform embeddings #
theorem
uniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
:
structure
UniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
extends
UniformInducing
:
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.
- comap_uniformity : Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (uniformity β) = uniformity α
- inj : Function.Injective f
A uniform embedding is injective.
Instances For
theorem
uniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
theorem
Filter.HasBasis.uniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : Filter.HasBasis (uniformity α) p s)
(h' : Filter.HasBasis (uniformity β) p' s')
{f : α → β}
:
theorem
Filter.HasBasis.uniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : Filter.HasBasis (uniformity α) p s)
(h' : Filter.HasBasis (uniformity β) p' s')
{f : α → β}
:
UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
theorem
uniformEmbedding_subtype_val
{α : Type u}
[UniformSpace α]
{p : α → Prop}
:
UniformEmbedding Subtype.val
theorem
uniformEmbedding_set_inclusion
{α : Type u}
[UniformSpace α]
{s : Set α}
{t : Set α}
(hst : s ⊆ t)
:
theorem
UniformEmbedding.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : UniformEmbedding g)
{f : α → β}
(hf : UniformEmbedding f)
:
UniformEmbedding (g ∘ f)
theorem
Equiv.uniformEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(h₁ : UniformContinuous ⇑f)
(h₂ : UniformContinuous ⇑f.symm)
:
theorem
uniformEmbedding_inl
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
:
UniformEmbedding Sum.inl
theorem
uniformEmbedding_inr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
:
UniformEmbedding Sum.inr
theorem
UniformInducing.uniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(hf : UniformInducing f)
:
If the domain of a UniformInducing map f is a T₀ space, then f is injective,
hence it is a UniformEmbedding.
theorem
uniformEmbedding_iff_uniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
:
theorem
comap_uniformity_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
Filter.comap (Prod.map f f) (uniformity β) = Filter.principal idRel
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
uniformEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (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
UniformEmbedding.embedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : UniformEmbedding f)
:
theorem
UniformEmbedding.denseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : UniformEmbedding f)
(hd : DenseRange f)
:
theorem
closedEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
[SeparatedSpace β]
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
theorem
closure_image_mem_nhds_of_uniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{s : Set (α × α)}
{e : α → β}
(b : β)
(he₁ : UniformInducing e)
(he₂ : DenseInducing e)
(hs : s ∈ uniformity α)
:
theorem
uniformEmbedding_subtypeEmb
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(p : α → Prop)
{e : α → β}
(ue : UniformEmbedding e)
(de : DenseEmbedding e)
:
theorem
UniformEmbedding.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : UniformEmbedding e₁)
(h₂ : UniformEmbedding e₂)
:
UniformEmbedding fun (p : α × β) => (e₁ p.1, e₂ p.2)
theorem
isComplete_of_complete_image
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : α → β}
{s : Set α}
(hm : UniformInducing m)
(hs : IsComplete (m '' s))
:
theorem
IsComplete.completeSpace_coe
{α : Type u}
[UniformSpace α]
{s : Set α}
(hs : IsComplete s)
:
theorem
isComplete_image_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : α → β}
{s : Set α}
(hm : UniformInducing m)
:
IsComplete (m '' s) ↔ IsComplete s
A set is complete iff its image under a uniform inducing map is complete.
theorem
completeSpace_iff_isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
:
CompleteSpace α ↔ IsComplete (Set.range f)
theorem
UniformInducing.isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
{f : α → β}
(hf : UniformInducing f)
:
IsComplete (Set.range f)
theorem
completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{e : α ≃ β}
(he : UniformEmbedding ⇑e)
:
theorem
completeSpace_coe_iff_isComplete
{α : Type u}
[UniformSpace α]
{s : Set α}
:
CompleteSpace ↑s ↔ IsComplete s
theorem
IsClosed.completeSpace_coe
{α : Type u}
[UniformSpace α]
[CompleteSpace α]
{s : Set α}
(hs : IsClosed s)
:
The lift of a complete space to another universe is still complete.
Equations
- (_ : CompleteSpace (ULift.{u_1, u} α)) = (_ : CompleteSpace (ULift.{u_1, u} α))
theorem
completeSpace_extension
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : β → α}
(hm : UniformInducing m)
(dense : DenseRange m)
(h : ∀ (f : Filter β), Cauchy f → ∃ (x : α), Filter.map m f ≤ nhds x)
:
theorem
totallyBounded_preimage
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set β}
(hf : UniformEmbedding f)
(hs : TotallyBounded s)
:
TotallyBounded (f ⁻¹' s)
instance
CompleteSpace.sum
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[CompleteSpace β]
:
CompleteSpace (α ⊕ β)
Equations
- (_ : CompleteSpace (α ⊕ β)) = (_ : CompleteSpace (α ⊕ β))
theorem
uniformEmbedding_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[u : UniformSpace β]
(hf : Function.Injective f)
:
def
Embedding.comapUniformSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(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
- Embedding.comapUniformSpace f h = UniformSpace.replaceTopology (UniformSpace.comap f u) (_ : inst = TopologicalSpace.induced f UniformSpace.toTopologicalSpace)
Instances For
theorem
Embedding.to_uniformEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Embedding f)
:
theorem
uniformly_extend_exists
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : UniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[CompleteSpace γ]
(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}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
[CompleteSpace γ]
{p : α → Prop}
{e : α → β}
{f : α → γ}
{b : β}
{s : Set α}
(hf : UniformContinuous fun (x : Subtype p) => f ↑x)
(he : UniformEmbedding e)
(hd : ∀ (x : β), x ∈ closure (Set.range e))
(hb : closure (e '' s) ∈ nhds b)
(hs : IsClosed s)
(hp : ∀ 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}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : UniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[CompleteSpace γ]
(a : α)
:
Filter.Tendsto f (Filter.comap e (nhds a)) (nhds (DenseInducing.extend (_ : DenseInducing e) f a))
theorem
uniformContinuous_uniformly_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : UniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[CompleteSpace γ]
:
UniformContinuous (DenseInducing.extend (_ : DenseInducing e) f)
theorem
uniformly_extend_of_ind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : UniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[SeparatedSpace γ]
(b : β)
:
DenseInducing.extend (_ : DenseInducing e) f (e b) = f b
theorem
uniformly_extend_unique
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : UniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
[SeparatedSpace γ]
{g : α → γ}
(hg : ∀ (b : β), g (e b) = f b)
(hc : Continuous g)
:
DenseInducing.extend (_ : DenseInducing e) f = g