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 IsUniformEmbedding.
- 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.comap_uniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(self : UniformInducing f)
:
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.
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 : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis 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.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : UniformInducing g)
{f : α → β}
:
UniformInducing (g ∘ f) ↔ UniformInducing f
theorem
UniformInducing.basis_uniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
{ι : Sort u_1}
{p : ι → Prop}
{s : ι → Set (β × β)}
(H : (uniformity β).HasBasis p s)
:
(uniformity α).HasBasis 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.uniformInducing_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : UniformInducing g)
:
UniformInducing (g ∘ f) ↔ UniformInducing 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.isDenseInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : UniformInducing f)
(hd : DenseRange f)
:
theorem
SeparationQuotient.uniformInducing_mk
{α : Type u}
[UniformSpace α]
:
UniformInducing SeparationQuotient.mk
theorem
UniformInducing.injective
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(h : UniformInducing f)
:
Uniform embeddings #
theorem
isUniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
:
structure
IsUniformEmbedding
{α : 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
IsUniformEmbedding.inj
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(self : IsUniformEmbedding f)
:
A uniform embedding is injective.
@[deprecated IsUniformEmbedding]
Alias of IsUniformEmbedding.
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.
Equations
Instances For
theorem
isUniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
@[deprecated isUniformEmbedding_iff']
theorem
uniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
Alias of isUniformEmbedding_iff'.
theorem
Filter.HasBasis.isUniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
@[deprecated Filter.HasBasis.isUniformEmbedding_iff']
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 : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
Alias of Filter.HasBasis.isUniformEmbedding_iff'.
theorem
Filter.HasBasis.isUniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
@[deprecated Filter.HasBasis.isUniformEmbedding_iff]
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 : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
Alias of Filter.HasBasis.isUniformEmbedding_iff.
theorem
isUniformEmbedding_subtype_val
{α : Type u}
[UniformSpace α]
{p : α → Prop}
:
IsUniformEmbedding Subtype.val
@[deprecated isUniformEmbedding_subtype_val]
theorem
uniformEmbedding_subtype_val
{α : Type u}
[UniformSpace α]
{p : α → Prop}
:
IsUniformEmbedding Subtype.val
Alias of isUniformEmbedding_subtype_val.
theorem
isUniformEmbedding_set_inclusion
{α : Type u}
[UniformSpace α]
{s : Set α}
{t : Set α}
(hst : s ⊆ t)
:
@[deprecated isUniformEmbedding_set_inclusion]
theorem
uniformEmbedding_set_inclusion
{α : Type u}
[UniformSpace α]
{s : Set α}
{t : Set α}
(hst : s ⊆ t)
:
Alias of isUniformEmbedding_set_inclusion.
theorem
IsUniformEmbedding.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
(hf : IsUniformEmbedding f)
:
IsUniformEmbedding (g ∘ f)
@[deprecated IsUniformEmbedding.comp]
theorem
UniformEmbedding.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
(hf : IsUniformEmbedding f)
:
IsUniformEmbedding (g ∘ f)
Alias of IsUniformEmbedding.comp.
theorem
IsUniformEmbedding.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
:
IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f
@[deprecated IsUniformEmbedding.of_comp_iff]
theorem
UniformEmbedding.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
:
IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f
Alias of IsUniformEmbedding.of_comp_iff.
theorem
Equiv.isUniformEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(h₁ : UniformContinuous ⇑f)
(h₂ : UniformContinuous ⇑f.symm)
:
@[deprecated Equiv.isUniformEmbedding]
theorem
Equiv.uniformEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(h₁ : UniformContinuous ⇑f)
(h₂ : UniformContinuous ⇑f.symm)
:
Alias of Equiv.isUniformEmbedding.
theorem
isUniformEmbedding_inl
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
:
IsUniformEmbedding Sum.inl
@[deprecated isUniformEmbedding_inl]
theorem
uniformEmbedding_inl
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
:
IsUniformEmbedding Sum.inl
Alias of isUniformEmbedding_inl.
theorem
isUniformEmbedding_inr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
:
IsUniformEmbedding Sum.inr
@[deprecated isUniformEmbedding_inr]
theorem
uniformEmbedding_inr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
:
IsUniformEmbedding Sum.inr
Alias of isUniformEmbedding_inr.
theorem
UniformInducing.isUniformEmbedding
{α : 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 IsUniformEmbedding.
@[deprecated UniformInducing.isUniformEmbedding]
theorem
UniformInducing.uniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(hf : UniformInducing f)
:
Alias of UniformInducing.isUniformEmbedding.
If the domain of a UniformInducing map f is a T₀ space, then f is injective,
hence it is a IsUniformEmbedding.
theorem
isUniformEmbedding_iff_uniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
:
@[deprecated isUniformEmbedding_iff_uniformInducing]
theorem
uniformEmbedding_iff_uniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
:
Alias of isUniformEmbedding_iff_uniformInducing.
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
isUniformEmbedding_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 α.
@[deprecated isUniformEmbedding_of_spaced_out]
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)
:
Alias of isUniformEmbedding_of_spaced_out.
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
IsUniformEmbedding.embedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
:
@[deprecated IsUniformEmbedding.embedding]
theorem
UniformEmbedding.embedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.embedding.
theorem
IsUniformEmbedding.isDenseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
(hd : DenseRange f)
:
@[deprecated IsUniformEmbedding.isDenseEmbedding]
theorem
UniformEmbedding.isDenseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
(hd : DenseRange f)
:
Alias of IsUniformEmbedding.isDenseEmbedding.
@[deprecated IsUniformEmbedding.isDenseEmbedding]
theorem
IsUniformEmbedding.denseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
(hd : DenseRange f)
:
Alias of IsUniformEmbedding.isDenseEmbedding.
theorem
closedEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
[T0Space β]
{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₂ : IsDenseInducing e)
(hs : s ∈ uniformity α)
:
theorem
isUniformEmbedding_subtypeEmb
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(p : α → Prop)
{e : α → β}
(ue : IsUniformEmbedding e)
(de : IsDenseEmbedding e)
:
@[deprecated isUniformEmbedding_subtypeEmb]
theorem
uniformEmbedding_subtypeEmb
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(p : α → Prop)
{e : α → β}
(ue : IsUniformEmbedding e)
(de : IsDenseEmbedding e)
:
Alias of isUniformEmbedding_subtypeEmb.
theorem
IsUniformEmbedding.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformEmbedding e₁)
(h₂ : IsUniformEmbedding e₂)
:
IsUniformEmbedding fun (p : α × β) => (e₁ p.1, e₂ p.2)
@[deprecated IsUniformEmbedding.prod]
theorem
UniformEmbedding.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformEmbedding e₁)
(h₂ : IsUniformEmbedding e₂)
:
IsUniformEmbedding fun (p : α × β) => (e₁ p.1, e₂ p.2)
Alias of IsUniformEmbedding.prod.
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
UniformInducing.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : UniformInducing f)
:
IsComplete (f '' s) ↔ IsComplete s
If f : X → Y is an UniformInducing map, the image f '' s of a set s is complete
if and only if s is complete.
theorem
IsUniformEmbedding.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformEmbedding f)
:
IsComplete (f '' s) ↔ IsComplete s
If f : X → Y is an IsUniformEmbedding, the image f '' s of a set s is complete
if and only if s is complete.
@[deprecated IsUniformEmbedding.isComplete_iff]
theorem
UniformEmbedding.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformEmbedding f)
:
IsComplete (f '' s) ↔ IsComplete s
Alias of IsUniformEmbedding.isComplete_iff.
If f : X → Y is an IsUniformEmbedding, the image f '' s of a set s is complete
if and only if s is complete.
theorem
Subtype.isComplete_iff
{α : Type u}
[UniformSpace α]
{p : α → Prop}
{s : Set { x : α // p x }}
:
IsComplete s ↔ IsComplete (Subtype.val '' s)
Sets of a subtype are complete iff their image under the coercion is complete.
theorem
isComplete_of_complete_image
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : α → β}
{s : Set α}
(hm : UniformInducing m)
:
IsComplete (m '' s) → IsComplete s
Alias of the forward direction of isComplete_image_iff.
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.completeSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
:
IsComplete (Set.range f) → CompleteSpace α
Alias of the reverse direction of completeSpace_iff_isComplete_range.
theorem
UniformInducing.isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
{f : α → β}
(hf : UniformInducing f)
:
IsComplete (Set.range f)
theorem
UniformInducing.completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformInducing f)
(hsurj : Function.Surjective f)
:
If f is a surjective uniform inducing map,
then its domain is a complete space iff its codomain is a complete space.
See also _root_.completeSpace_congr for a version that assumes f to be an equivalence.
Equations
- ⋯ = ⋯
theorem
completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{e : α ≃ β}
(he : IsUniformEmbedding ⇑e)
:
See also UniformInducing.completeSpace_congr
for a version that works for non-injective maps.
theorem
completeSpace_coe_iff_isComplete
{α : Type u}
[UniformSpace α]
{s : Set α}
:
CompleteSpace ↑s ↔ IsComplete s
theorem
IsComplete.completeSpace_coe
{α : Type u}
[UniformSpace α]
{s : Set α}
:
IsComplete s → CompleteSpace ↑s
Alias of the reverse direction of completeSpace_coe_iff_isComplete.
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
- ⋯ = ⋯
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_image_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : UniformInducing f)
:
TotallyBounded (f '' s) ↔ TotallyBounded s
theorem
totallyBounded_preimage
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set β}
(hf : UniformInducing f)
(hs : TotallyBounded s)
:
TotallyBounded (f ⁻¹' s)
instance
CompleteSpace.sum
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[CompleteSpace β]
:
CompleteSpace (α ⊕ β)
Equations
- ⋯ = ⋯
theorem
isUniformEmbedding_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[u : UniformSpace β]
(hf : Function.Injective f)
:
@[deprecated isUniformEmbedding_comap]
theorem
uniformEmbedding_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[u : UniformSpace β]
(hf : Function.Injective f)
:
Alias of isUniformEmbedding_comap.
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.comap f u).replaceTopology ⋯
Instances For
theorem
Embedding.to_isUniformEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Embedding f)
:
@[deprecated Embedding.to_isUniformEmbedding]
theorem
Embedding.to_uniformEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Embedding f)
:
Alias of Embedding.to_isUniformEmbedding.
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 : IsUniformEmbedding 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 (⋯.extend 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 (⋯.extend 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)
[T0Space γ]
(b : β)
:
⋯.extend 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 : β → γ}
[T0Space γ]
{g : α → γ}
(hg : ∀ (b : β), g (e b) = f b)
(hc : Continuous g)
:
⋯.extend f = g