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 UniformEmbedding.

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.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.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 #

    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.

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

      A uniform embedding is injective.

      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 : αβ} :
      UniformEmbedding 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
      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 : αβ} :
      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) :
      theorem UniformEmbedding.of_comp_iff {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {g : βγ} (hg : 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 β] :
      theorem uniformEmbedding_inr {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] :
      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 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 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 α] [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₂ : DenseInducing e) (hs : s uniformity α) :
      ∃ (a : α), closure (e '' {a' : α | (a, a') s}) nhds b
      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_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 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.isComplete_range {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [CompleteSpace α] {f : αβ} (hf : UniformInducing f) :
      theorem completeSpace_congr {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {e : α β} (he : UniformEmbedding e) :
      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_preimage {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} {s : Set β} (hf : UniformEmbedding f) (hs : TotallyBounded s) :
      instance CompleteSpace.sum {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [CompleteSpace α] [CompleteSpace β] :
      Equations
      • =
      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
      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 : 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