Documentation

Mathlib.Topology.UniformSpace.UniformEmbedding

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 α
structure UniformInducing {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] (f : αβ) :

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.

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 fUniformSpace.comap f inst✝ = inst✝¹

    Alias of the forward direction of uniformInducing_iff_uniformSpace.

    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 : αβ} :
    UniformInducing f (∀ (i : ι'), p' i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (j : ι), p j∃ (i : ι'), p' i ∀ (x y : α), (f x, f y) s' i(x, y) s j
    theorem UniformInducing.mk' {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} (h : ∀ (s : Set (α × α)), s uniformity α tuniformity β, ∀ (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) :
    theorem UniformInducing.of_comp_iff {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {g : βγ} (hg : 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 : (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 α} :
    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) :
    theorem UniformInducing.uniformInducing_comp_iff {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : αβ} {g : βγ} (hg : UniformInducing g) :
    theorem UniformInducing.uniformContinuousOn_iff {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : αβ} {g : βγ} {S : Set α} (hg : UniformInducing g) :
    theorem UniformInducing.inducing {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} (h : UniformInducing 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 UniformInducing.injective {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [T0Space α] {f : αβ} (h : UniformInducing f) :

    Uniform embeddings #

    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.

    Instances For
      theorem IsUniformEmbedding.inj {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} (self : IsUniformEmbedding f) :

      A uniform embedding is injective.

      @[deprecated IsUniformEmbedding]
      def UniformEmbedding {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] (f : αβ) :

      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
        @[deprecated isUniformEmbedding_iff']

        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 : αβ} :
        IsUniformEmbedding f Function.Injective f (∀ (i : ι'), p' i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (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 (∀ (i : ι'), p' i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) s' i) ∀ (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 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) :
        @[deprecated IsUniformEmbedding.comp]
        theorem UniformEmbedding.comp {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {g : βγ} (hg : IsUniformEmbedding g) {f : αβ} (hf : IsUniformEmbedding f) :

        Alias of IsUniformEmbedding.comp.

        theorem IsUniformEmbedding.of_comp_iff {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {g : βγ} (hg : IsUniformEmbedding g) {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 : αβ} :

        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.

        @[deprecated isUniformEmbedding_inl]
        theorem uniformEmbedding_inl {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] :

        Alias of isUniformEmbedding_inl.

        @[deprecated isUniformEmbedding_inr]
        theorem uniformEmbedding_inr {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] :

        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.

        @[deprecated isUniformEmbedding_iff_uniformInducing]

        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) :

        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 α) :
        ∃ (a : α), closure (e '' {a' : α | (a, a') s}) nhds b
        @[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) :

        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) :

        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) :

        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) :

        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) :

        Alias of the forward direction of isComplete_image_iff.


        A set is complete iff its image under a uniform inducing map is complete.

        theorem UniformInducing.completeSpace {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} (hf : UniformInducing f) :

        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) :
        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.

        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 IsComplete.completeSpace_coe {α : Type u} [UniformSpace α] {s : Set α} :

        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) :
        theorem totallyBounded_preimage {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} {s : Set β} (hf : UniformInducing f) (hs : TotallyBounded s) :
        instance CompleteSpace.sum {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [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
        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 : xs, 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