Uniform embeddings of uniform spaces. #
Extension of uniform continuous functions.
Uniform inducing maps #
theorem
isUniformInducing_iff_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
theorem
IsUniformInducing.comap_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformInducing f → UniformSpace.comap f inst✝ = inst✝¹
Alias of the forward direction of isUniformInducing_iff_uniformSpace.
theorem
isUniformInducing_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
theorem
Filter.HasBasis.isUniformInducing_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
IsUniformInducing.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
IsUniformInducing.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
(hf : IsUniformInducing f)
:
IsUniformInducing (g ∘ f)
theorem
IsUniformInducing.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
:
theorem
IsUniformInducing.basis_uniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing 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
IsUniformInducing.cauchy_map_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
{F : Filter α}
:
theorem
IsUniformInducing.of_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
(hgf : IsUniformInducing (g ∘ f))
:
theorem
IsUniformInducing.uniformContinuous
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
theorem
IsUniformInducing.uniformContinuous_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : IsUniformInducing g)
:
@[deprecated IsUniformInducing.of_comp_iff (since := "2026-03-17")]
theorem
IsUniformInducing.isUniformInducing_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
:
Alias of IsUniformInducing.of_comp_iff.
theorem
IsUniformInducing.uniformContinuousOn_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
{S : Set α}
(hg : IsUniformInducing g)
:
theorem
IsUniformInducing.isInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
:
theorem
IsUniformInducing.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformInducing e₁)
(h₂ : IsUniformInducing e₂)
:
IsUniformInducing fun (p : α × β) => (e₁ p.1, e₂ p.2)
theorem
IsUniformInducing.isDenseInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
(hd : DenseRange f)
:
theorem
IsUniformInducing.injective
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(h : IsUniformInducing f)
:
Uniform embeddings #
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 α
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 : α → β}
:
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
theorem
isUniformEmbedding_set_inclusion
{α : Type u}
[UniformSpace α]
{s t : Set α}
(hst : s ⊆ t)
:
theorem
IsUniformEmbedding.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
(hf : IsUniformEmbedding f)
:
IsUniformEmbedding (g ∘ f)
theorem
IsUniformEmbedding.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
:
theorem
IsUniformEmbedding.of_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
(hgf : IsUniformEmbedding (g ∘ f))
:
theorem
Equiv.isUniformEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(h₁ : UniformContinuous ⇑f)
(h₂ : UniformContinuous ⇑f.symm)
:
theorem
IsUniformInducing.isUniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(hf : IsUniformInducing f)
:
If the domain of a IsUniformInducing map f is a T₀ space, then f is injective,
hence it is a IsUniformEmbedding.
theorem
isUniformEmbedding_iff_isUniformInducing
{α : 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)
:
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 α.
theorem
IsUniformEmbedding.isEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
:
theorem
IsUniformEmbedding.isDenseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
(hd : DenseRange f)
:
theorem
isClosedEmbedding_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_isUniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{s : Set (α × α)}
{e : α → β}
(b : β)
(he₁ : IsUniformInducing 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)
:
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)
theorem
isComplete_image_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : α → β}
{s : Set α}
(hm : IsUniformInducing m)
:
A set is complete iff its image under a uniform inducing map is complete.
theorem
IsUniformInducing.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformInducing f)
:
If f : X → Y is an IsUniformInducing 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)
:
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 }}
:
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 : IsUniformInducing 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 : IsUniformInducing f)
:
theorem
IsUniformInducing.completeSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
IsComplete (Set.range f) → CompleteSpace α
Alias of the reverse direction of completeSpace_iff_isComplete_range.
theorem
IsUniformInducing.isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
[CompleteSpace α]
(hf : IsUniformInducing f)
:
IsComplete (Set.range f)
theorem
IsUniformInducing.completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing 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.
theorem
completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{e : α ≃ β}
(he : IsUniformEmbedding ⇑e)
:
See also IsUniformInducing.completeSpace_congr
for a version that works for non-injective maps.
theorem
IsComplete.completeSpace_coe
{α : Type u}
[UniformSpace α]
{s : Set α}
:
IsComplete s → CompleteSpace ↑s
Alias of the reverse direction of completeSpace_coe_iff_isComplete.
instance
IsClosed.completeSpace_coe
{α : Type u}
[UniformSpace α]
[CompleteSpace α]
{s : Set α}
[hs : IsClosed s]
:
The lift of a complete space to another universe is still complete.
theorem
completeSpace_extension
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : β → α}
(hm : IsUniformInducing m)
(dense : DenseRange m)
(h : ∀ (f : Filter β), Cauchy f → ∃ (x : α), Filter.map m f ≤ nhds x)
:
theorem
Filter.totallyBounded_map_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{F : Filter α}
(hf : IsUniformInducing f)
:
theorem
totallyBounded_image_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformInducing f)
:
theorem
totallyBounded_preimage
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set β}
(hf : IsUniformInducing f)
(hs : TotallyBounded s)
:
TotallyBounded (f ⁻¹' s)
theorem
Filter.totallyBounded_comap
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{F : Filter β}
(hf : IsUniformInducing f)
(hF : F.TotallyBounded)
:
(comap f F).TotallyBounded
instance
CompleteSpace.sum
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[CompleteSpace β]
:
CompleteSpace (α ⊕ β)
theorem
IsUniformEmbedding.discreteUniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[DiscreteUniformity β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
theorem
isUniformEmbedding_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[u : UniformSpace β]
(hf : Function.Injective f)
:
@[instance_reducible]
def
Topology.IsEmbedding.comapUniformSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : IsEmbedding 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
Instances For
theorem
Embedding.to_isUniformEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Topology.IsEmbedding f)
:
theorem
uniformly_extend_exists
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing 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 : IsUniformInducing 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 : IsUniformInducing 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 : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[T0Space γ]
(b : β)
:
theorem
uniformly_extend_unique
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
[T0Space γ]
{g : α → γ}
(hg : ∀ (b : β), g (e b) = f b)
(hc : Continuous g)
:
@[simp]
theorem
uniformContinuous_rangeFactorization_iff
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
theorem
UniformContinuous.rangeFactorization
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformContinuous f)
:
@[simp]
theorem
isUniformInducing_rangeFactorization_iff
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
theorem
IsUniformInducing.rangeFactorization
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
theorem
Dense.extend_exists
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[CompleteSpace β]
(hs : Dense s)
(hf : UniformContinuous f)
(a : α)
:
∃ (b : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)
theorem
Dense.extend_spec
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[CompleteSpace β]
(hs : Dense s)
(hf : UniformContinuous f)
(a : α)
:
Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds (hs.extend f a))
theorem
Dense.uniformContinuous_extend
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[CompleteSpace β]
(hs : Dense s)
(hf : UniformContinuous f)
:
UniformContinuous (hs.extend f)
theorem
Dense.extend_of_ind
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[T0Space β]
(hs : Dense s)
(hf : UniformContinuous f)
(x : ↑s)
:
theorem
IsDenseInducing.isUniformInducing_extend
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
[CompleteSpace β]
[CompleteSpace γ]
{i : α → β}
{f : α → γ}
(hid : IsDenseInducing i)
(hi : IsUniformInducing i)
(h : IsUniformInducing f)
:
IsUniformInducing (hid.extend f)