Documentation

Mathlib.Topology.UniformSpace.Basic

Uniform spaces #

Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly generalize to uniform spaces, e.g.

A uniform structure on a type X is a filter 𝓤 X on X × X satisfying some conditions which makes it reasonable to say that ∀ᶠ (p : X × X) in 𝓤 X, ... means "for all p.1 and p.2 in X close enough, ...". Elements of this filter are called entourages of X. The two main examples are:

Those examples are generalizations in two different directions of the elementary example where X = ℝ and V ∈ 𝓤 ℝ ↔ ∃ ε > 0, { p | |p.2 - p.1| < ε } ⊆ V which features both the topological group structure on and its metric space structure.

Each uniform structure on X induces a topology on X characterized by

nhds_eq_comap_uniformity : ∀ {x : X}, 𝓝 x = comap (Prod.mk x) (𝓤 X)

where Prod.mk x : X → X × X := (fun y ↦ (x, y)) is the partial evaluation of the product constructor.

The dictionary with metric spaces includes:

The triangle inequality is abstracted to a statement involving the composition of relations in X. First note that the triangle inequality in a metric space is equivalent to ∀ (x y z : X) (r r' : ℝ), dist x y ≤ r → dist y z ≤ r' → dist x z ≤ r + r'. Then, for any V and W with type Set (X × X), the composition V ○ W : Set (X × X) is defined as { p : X × X | ∃ z, (p.1, z) ∈ V ∧ (z, p.2) ∈ W }. In the metric space case, if V = { p | dist p.1 p.2 ≤ r } and W = { p | dist p.1 p.2 ≤ r' } then the triangle inequality, as reformulated above, says V ○ W is contained in {p | dist p.1 p.2 ≤ r + r'} which is the entourage associated to the radius r + r'. In general we have mem_ball_comp (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (V ○ W). Note that this discussion does not depend on any axiom imposed on the uniformity filter, it is simply captured by the definition of composition.

The uniform space axioms ask the filter 𝓤 X to satisfy the following:

These three axioms are stated more abstractly in the definition below, in terms of operations on filters, without directly manipulating entourages.

Main definitions #

In this file we also define a complete lattice structure on the type UniformSpace X of uniform structures on X, as well as the pullback (UniformSpace.comap) of uniform structures coming from the pullback of filters. Like distance functions, uniform structures cannot be pushed forward in general.

Notations #

Localized in Uniformity, we have the notation 𝓤 X for the uniformity on a uniform space X, and for composition of relations, seen as terms with type Set (X × X).

Implementation notes #

There is already a theory of relations in Data/Rel.lean where the main definition is def Rel (α β : Type*) := α → β → Prop. The relations used in the current file involve only one type, but this is not the reason why we don't reuse Data/Rel.lean. We use Set (α × α) instead of Rel α α because we really need sets to use the filter library, and elements of filters on α × α have type Set (α × α).

The structure UniformSpace X bundles a uniform structure on X, a topology on X and an assumption saying those are compatible. This may not seem mathematically reasonable at first, but is in fact an instance of the forgetful inheritance pattern. See Note [forgetful inheritance] below.

References #

The formalization uses the books:

But it makes a more systematic use of the filter library.

Relations, seen as Set (α × α) #

def idRel {α : Type u_2} :
Set (α × α)

The identity relation, or the graph of the identity function

Equations
  • idRel = {p : α × α | p.1 = p.2}
Instances For
    @[simp]
    theorem mem_idRel {α : Type ua} {a : α} {b : α} :
    (a, b) idRel a = b
    @[simp]
    theorem idRel_subset {α : Type ua} {s : Set (α × α)} :
    idRel s ∀ (a : α), (a, a) s
    theorem eq_singleton_left_of_prod_subset_idRel {X : Type u_2} {S : Set X} {T : Set X} (hS : S.Nonempty) (hT : T.Nonempty) (h_diag : S ×ˢ T idRel) :
    ∃ (x : X), S = {x}
    theorem eq_singleton_right_prod_subset_idRel {X : Type u_2} {S : Set X} {T : Set X} (hS : S.Nonempty) (hT : T.Nonempty) (h_diag : S ×ˢ T idRel) :
    ∃ (x : X), T = {x}
    theorem eq_singleton_prod_subset_idRel {X : Type u_2} {S : Set X} {T : Set X} (hS : S.Nonempty) (hT : T.Nonempty) (h_diag : S ×ˢ T idRel) :
    ∃ (x : X), S = {x} T = {x}
    def compRel {α : Type ua} (r₁ : Set (α × α)) (r₂ : Set (α × α)) :
    Set (α × α)

    The composition of relations

    Equations
    Instances For

      The composition of relations

      Equations
      Instances For
        @[simp]
        theorem mem_compRel {α : Type u} {r₁ : Set (α × α)} {r₂ : Set (α × α)} {x : α} {y : α} :
        (x, y) compRel r₁ r₂ ∃ (z : α), (x, z) r₁ (z, y) r₂
        @[simp]
        theorem swap_idRel {α : Type ua} :
        Prod.swap '' idRel = idRel
        theorem Monotone.compRel {α : Type ua} {β : Type ub} [Preorder β] {f : βSet (α × α)} {g : βSet (α × α)} (hf : Monotone f) (hg : Monotone g) :
        Monotone fun (x : β) => compRel (f x) (g x)
        theorem compRel_mono {α : Type ua} {f : Set (α × α)} {g : Set (α × α)} {h : Set (α × α)} {k : Set (α × α)} (h₁ : f h) (h₂ : g k) :
        theorem prod_mk_mem_compRel {α : Type ua} {a : α} {b : α} {c : α} {s : Set (α × α)} {t : Set (α × α)} (h₁ : (a, c) s) (h₂ : (c, b) t) :
        (a, b) compRel s t
        @[simp]
        theorem id_compRel {α : Type ua} {r : Set (α × α)} :
        compRel idRel r = r
        theorem compRel_assoc {α : Type ua} {r : Set (α × α)} {s : Set (α × α)} {t : Set (α × α)} :
        compRel (compRel r s) t = compRel r (compRel s t)
        theorem left_subset_compRel {α : Type ua} {s : Set (α × α)} {t : Set (α × α)} (h : idRel t) :
        s compRel s t
        theorem right_subset_compRel {α : Type ua} {s : Set (α × α)} {t : Set (α × α)} (h : idRel s) :
        t compRel s t
        theorem subset_comp_self {α : Type ua} {s : Set (α × α)} (h : idRel s) :
        s compRel s s
        theorem subset_iterate_compRel {α : Type ua} {s : Set (α × α)} {t : Set (α × α)} (h : idRel s) (n : ) :
        t (fun (x : Set (α × α)) => compRel s x)^[n] t
        def SymmetricRel {α : Type ua} (V : Set (α × α)) :

        The relation is invariant under swapping factors.

        Equations
        Instances For
          def symmetrizeRel {α : Type ua} (V : Set (α × α)) :
          Set (α × α)

          The maximal symmetric relation contained in a given relation.

          Equations
          Instances For
            theorem symmetric_symmetrizeRel {α : Type ua} (V : Set (α × α)) :
            theorem symmetrizeRel_subset_self {α : Type ua} (V : Set (α × α)) :
            theorem symmetrize_mono {α : Type ua} {V : Set (α × α)} {W : Set (α × α)} (h : V W) :
            theorem SymmetricRel.mk_mem_comm {α : Type ua} {V : Set (α × α)} (hV : SymmetricRel V) {x : α} {y : α} :
            (x, y) V (y, x) V
            theorem SymmetricRel.eq {α : Type ua} {U : Set (α × α)} (hU : SymmetricRel U) :
            Prod.swap ⁻¹' U = U
            theorem SymmetricRel.inter {α : Type ua} {U : Set (α × α)} {V : Set (α × α)} (hU : SymmetricRel U) (hV : SymmetricRel V) :
            structure UniformSpace.Core (α : Type u) :

            This core description of a uniform space is outside of the type class hierarchy. It is useful for constructions of uniform spaces, when the topology is derived from the uniform space.

            Instances For
              theorem UniformSpace.Core.refl {α : Type u} (self : UniformSpace.Core α) :
              Filter.principal idRel self.uniformity

              Every set in the uniformity filter includes the diagonal.

              theorem UniformSpace.Core.symm {α : Type u} (self : UniformSpace.Core α) :
              Filter.Tendsto Prod.swap self.uniformity self.uniformity

              If s ∈ uniformity, then Prod.swap ⁻¹' s ∈ uniformity.

              theorem UniformSpace.Core.comp {α : Type u} (self : UniformSpace.Core α) :
              (self.uniformity.lift' fun (s : Set (α × α)) => compRel s s) self.uniformity

              For every set u ∈ uniformity, there exists v ∈ uniformity such that v ○ v ⊆ u.

              theorem UniformSpace.Core.comp_mem_uniformity_sets {α : Type ua} {c : UniformSpace.Core α} {s : Set (α × α)} (hs : s c.uniformity) :
              tc.uniformity, compRel t t s
              def UniformSpace.Core.mk' {α : Type u} (U : Filter (α × α)) (refl : rU, ∀ (x : α), (x, x) r) (symm : rU, Prod.swap ⁻¹' r U) (comp : rU, tU, compRel t t r) :

              An alternative constructor for UniformSpace.Core. This version unfolds various Filter-related definitions.

              Equations
              Instances For
                def UniformSpace.Core.mkOfBasis {α : Type u} (B : FilterBasis (α × α)) (refl : rB, ∀ (x : α), (x, x) r) (symm : rB, tB, t Prod.swap ⁻¹' r) (comp : rB, tB, compRel t t r) :

                Defining a UniformSpace.Core from a filter basis satisfying some uniformity-like axioms.

                Equations
                Instances For

                  A uniform space generates a topological space

                  Equations
                  Instances For
                    theorem UniformSpace.Core.ext {α : Type ua} {u₁ : UniformSpace.Core α} {u₂ : UniformSpace.Core α} :
                    u₁.uniformity = u₂.uniformityu₁ = u₂
                    class UniformSpace (α : Type u) extends TopologicalSpace :

                    A uniform space is a generalization of the "uniform" topological aspects of a metric space. It consists of a filter on α × α called the "uniformity", which satisfies properties analogous to the reflexivity, symmetry, and triangle properties of a metric.

                    A metric space has a natural uniformity, and a uniform space has a natural topology. A topological group also has a natural uniformity, even when it is not metrizable.

                    Instances
                      theorem UniformSpace.symm {α : Type u} [self : UniformSpace α] :
                      Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity

                      If s ∈ uniformity, then Prod.swap ⁻¹' s ∈ uniformity.

                      theorem UniformSpace.comp {α : Type u} [self : UniformSpace α] :
                      (UniformSpace.uniformity.lift' fun (s : Set (α × α)) => compRel s s) UniformSpace.uniformity

                      For every set u ∈ uniformity, there exists v ∈ uniformity such that v ○ v ⊆ u.

                      theorem UniformSpace.nhds_eq_comap_uniformity {α : Type u} [self : UniformSpace α] (x : α) :
                      nhds x = Filter.comap (Prod.mk x) UniformSpace.uniformity

                      The uniformity agrees with the topology: the neighborhoods filter of each point x is equal to Filter.comap (Prod.mk x) (𝓤 α).

                      def uniformity (α : Type u) [UniformSpace α] :
                      Filter (α × α)

                      The uniformity is a filter on α × α (inferred from an ambient uniform space structure on α).

                      Equations
                      Instances For

                        Notation for the uniformity filter with respect to a non-standard UniformSpace instance.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The uniformity is a filter on α × α (inferred from an ambient uniform space structure on α).

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev UniformSpace.ofCoreEq {α : Type u} (u : UniformSpace.Core α) (t : TopologicalSpace α) (h : t = u.toTopologicalSpace) :

                            Construct a UniformSpace from a u : UniformSpace.Core and a TopologicalSpace structure that is equal to u.toTopologicalSpace.

                            Equations
                            Instances For
                              @[reducible, inline]

                              Construct a UniformSpace from a UniformSpace.Core.

                              Equations
                              Instances For
                                @[reducible, inline]

                                Construct a UniformSpace.Core from a UniformSpace.

                                Equations
                                • u.toCore = { uniformity := UniformSpace.uniformity, refl := , symm := , comp := }
                                Instances For
                                  theorem UniformSpace.toCore_toTopologicalSpace {α : Type ua} (u : UniformSpace α) :
                                  u.toCore.toTopologicalSpace = UniformSpace.toTopologicalSpace
                                  @[deprecated UniformSpace.mk]
                                  def UniformSpace.ofNhdsEqComap {α : Type ua} (u : UniformSpace.Core α) (_t : TopologicalSpace α) (h : ∀ (x : α), nhds x = Filter.comap (Prod.mk x) u.uniformity) :

                                  Build a UniformSpace from a UniformSpace.Core and a compatible topology. Use UniformSpace.mk instead to avoid proving the unnecessary assumption UniformSpace.Core.refl.

                                  The main constructor used to use a different compatibility assumption. This definition was created as a step towards porting to a new definition. Now the main definition is ported, so this constructor will be removed in a few months.

                                  Equations
                                  Instances For
                                    theorem UniformSpace.ext {α : Type ua} {u₁ : UniformSpace α} {u₂ : UniformSpace α} (h : uniformity α = uniformity α) :
                                    u₁ = u₂
                                    theorem UniformSpace.ext_iff {α : Type ua} {u₁ : UniformSpace α} {u₂ : UniformSpace α} :
                                    u₁ = u₂ ∀ (s : Set (α × α)), s uniformity α s uniformity α
                                    theorem UniformSpace.ofCoreEq_toCore {α : Type ua} (u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace) :
                                    UniformSpace.ofCoreEq u.toCore t h = u
                                    @[reducible, inline]
                                    abbrev UniformSpace.replaceTopology {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = UniformSpace.toTopologicalSpace) :

                                    Replace topology in a UniformSpace instance with a propositionally (but possibly not definitionally) equal one.

                                    Equations
                                    Instances For
                                      theorem UniformSpace.replaceTopology_eq {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = UniformSpace.toTopologicalSpace) :
                                      u.replaceTopology h = u
                                      theorem isOpen_uniformity {α : Type ua} [UniformSpace α] {s : Set α} :
                                      IsOpen s xs, {p : α × α | p.1 = xp.2 s} uniformity α
                                      instance uniformity.neBot {α : Type ua} [UniformSpace α] [Nonempty α] :
                                      (uniformity α).NeBot
                                      Equations
                                      • =
                                      theorem refl_mem_uniformity {α : Type ua} [UniformSpace α] {x : α} {s : Set (α × α)} (h : s uniformity α) :
                                      (x, x) s
                                      theorem mem_uniformity_of_eq {α : Type ua} [UniformSpace α] {x : α} {y : α} {s : Set (α × α)} (h : s uniformity α) (hx : x = y) :
                                      (x, y) s
                                      theorem comp_le_uniformity {α : Type ua} [UniformSpace α] :
                                      ((uniformity α).lift' fun (s : Set (α × α)) => compRel s s) uniformity α
                                      theorem lift'_comp_uniformity {α : Type ua} [UniformSpace α] :
                                      ((uniformity α).lift' fun (s : Set (α × α)) => compRel s s) = uniformity α
                                      theorem comp_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      tuniformity α, compRel t t s
                                      theorem eventually_uniformity_iterate_comp_subset {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) (n : ) :
                                      ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, (fun (x : Set (α × α)) => compRel t x)^[n] t s

                                      If s ∈ 𝓤 α, then for any natural n, for a subset t of a sufficiently small set in 𝓤 α, we have t ○ t ○ ... ○ t ⊆ s (n compositions).

                                      theorem eventually_uniformity_comp_subset {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, compRel t t s

                                      If s ∈ 𝓤 α, then for a subset t of a sufficiently small set in 𝓤 α, we have t ○ t ⊆ s.

                                      theorem Filter.Tendsto.uniformity_trans {α : Type ua} {β : Type ub} [UniformSpace α] {l : Filter β} {f₁ : βα} {f₂ : βα} {f₃ : βα} (h₁₂ : Filter.Tendsto (fun (x : β) => (f₁ x, f₂ x)) l (uniformity α)) (h₂₃ : Filter.Tendsto (fun (x : β) => (f₂ x, f₃ x)) l (uniformity α)) :
                                      Filter.Tendsto (fun (x : β) => (f₁ x, f₃ x)) l (uniformity α)

                                      Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is transitive.

                                      theorem Filter.Tendsto.uniformity_symm {α : Type ua} {β : Type ub} [UniformSpace α] {l : Filter β} {f : βα × α} (h : Filter.Tendsto f l (uniformity α)) :
                                      Filter.Tendsto (fun (x : β) => ((f x).2, (f x).1)) l (uniformity α)

                                      Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is symmetric.

                                      theorem tendsto_diag_uniformity {α : Type ua} {β : Type ub} [UniformSpace α] (f : βα) (l : Filter β) :
                                      Filter.Tendsto (fun (x : β) => (f x, f x)) l (uniformity α)

                                      Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is reflexive.

                                      theorem tendsto_const_uniformity {α : Type ua} {β : Type ub} [UniformSpace α] {a : α} {f : Filter β} :
                                      Filter.Tendsto (fun (x : β) => (a, a)) f (uniformity α)
                                      theorem symm_of_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      tuniformity α, (∀ (a b : α), (a, b) t(b, a) t) t s
                                      theorem comp_symm_of_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      tuniformity α, (∀ {a b : α}, (a, b) t(b, a) t) compRel t t s
                                      theorem uniformity_le_symm {α : Type ua} [UniformSpace α] :
                                      uniformity α Prod.swap <$> uniformity α
                                      theorem uniformity_eq_symm {α : Type ua} [UniformSpace α] :
                                      uniformity α = Prod.swap <$> uniformity α
                                      @[simp]
                                      theorem comap_swap_uniformity {α : Type ua} [UniformSpace α] :
                                      theorem symmetrize_mem_uniformity {α : Type ua} [UniformSpace α] {V : Set (α × α)} (h : V uniformity α) :
                                      theorem UniformSpace.hasBasis_symmetric {α : Type ua} [UniformSpace α] :
                                      (uniformity α).HasBasis (fun (s : Set (α × α)) => s uniformity α SymmetricRel s) id

                                      Symmetric entourages form a basis of 𝓤 α

                                      theorem uniformity_lift_le_swap {α : Type ua} {β : Type ub} [UniformSpace α] {g : Set (α × α)Filter β} {f : Filter β} (hg : Monotone g) (h : ((uniformity α).lift fun (s : Set (α × α)) => g (Prod.swap ⁻¹' s)) f) :
                                      (uniformity α).lift g f
                                      theorem uniformity_lift_le_comp {α : Type ua} {β : Type ub} [UniformSpace α] {f : Set (α × α)Filter β} (h : Monotone f) :
                                      ((uniformity α).lift fun (s : Set (α × α)) => f (compRel s s)) (uniformity α).lift f
                                      theorem comp3_mem_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      tuniformity α, compRel t (compRel t t) s
                                      theorem comp_le_uniformity3 {α : Type ua} [UniformSpace α] :
                                      ((uniformity α).lift' fun (s : Set (α × α)) => compRel s (compRel s s)) uniformity α

                                      See also comp3_mem_uniformity.

                                      theorem comp_symm_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      tuniformity α, SymmetricRel t compRel t t s

                                      See also comp_open_symm_mem_uniformity_sets.

                                      theorem subset_comp_self_of_mem_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (h : s uniformity α) :
                                      s compRel s s
                                      theorem comp_comp_symm_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                      tuniformity α, SymmetricRel t compRel (compRel t t) t s

                                      Balls in uniform spaces #

                                      def UniformSpace.ball {β : Type ub} (x : β) (V : Set (β × β)) :
                                      Set β

                                      The ball around (x : β) with respect to (V : Set (β × β)). Intended to be used for V ∈ 𝓤 β, but this is not needed for the definition. Recovers the notions of metric space ball when V = {p | dist p.1 p.2 < r }.

                                      Equations
                                      Instances For
                                        theorem UniformSpace.mem_ball_self {α : Type ua} [UniformSpace α] (x : α) {V : Set (α × α)} :
                                        theorem UniformSpace.mem_ball_comp {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {x : β} {y : β} {z : β} (h : y UniformSpace.ball x V) (h' : z UniformSpace.ball y W) :

                                        The triangle inequality for UniformSpace.ball

                                        theorem UniformSpace.ball_subset_of_comp_subset {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {x : β} {y : β} (h : x UniformSpace.ball y W) (h' : compRel W W V) :
                                        theorem UniformSpace.ball_mono {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} (h : V W) (x : β) :
                                        theorem UniformSpace.ball_inter {β : Type ub} (x : β) (V : Set (β × β)) (W : Set (β × β)) :
                                        theorem UniformSpace.ball_inter_left {β : Type ub} (x : β) (V : Set (β × β)) (W : Set (β × β)) :
                                        theorem UniformSpace.ball_inter_right {β : Type ub} (x : β) (V : Set (β × β)) (W : Set (β × β)) :
                                        theorem UniformSpace.mem_ball_symmetry {β : Type ub} {V : Set (β × β)} (hV : SymmetricRel V) {x : β} {y : β} :
                                        theorem UniformSpace.ball_eq_of_symmetry {β : Type ub} {V : Set (β × β)} (hV : SymmetricRel V) {x : β} :
                                        UniformSpace.ball x V = {y : β | (y, x) V}
                                        theorem UniformSpace.mem_comp_of_mem_ball {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {x : β} {y : β} {z : β} (hV : SymmetricRel V) (hx : x UniformSpace.ball z V) (hy : y UniformSpace.ball z W) :
                                        (x, y) compRel V W
                                        theorem UniformSpace.isOpen_ball {α : Type ua} [UniformSpace α] (x : α) {V : Set (α × α)} (hV : IsOpen V) :
                                        theorem UniformSpace.isClosed_ball {α : Type ua} [UniformSpace α] (x : α) {V : Set (α × α)} (hV : IsClosed V) :
                                        theorem UniformSpace.mem_comp_comp {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {M : Set (β × β)} (hW' : SymmetricRel W) {p : β × β} :
                                        p compRel (compRel V M) W (UniformSpace.ball p.1 V ×ˢ UniformSpace.ball p.2 W M).Nonempty

                                        Neighborhoods in uniform spaces #

                                        theorem mem_nhds_uniformity_iff_right {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
                                        s nhds x {p : α × α | p.1 = xp.2 s} uniformity α
                                        theorem mem_nhds_uniformity_iff_left {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
                                        s nhds x {p : α × α | p.2 = xp.1 s} uniformity α
                                        theorem nhdsWithin_eq_comap_uniformity_of_mem {α : Type ua} [UniformSpace α] {x : α} {T : Set α} (hx : x T) (S : Set α) :
                                        theorem nhdsWithin_eq_comap_uniformity {α : Type ua} [UniformSpace α] {x : α} (S : Set α) :
                                        theorem isOpen_iff_ball_subset {α : Type ua} [UniformSpace α] {s : Set α} :
                                        IsOpen s xs, Vuniformity α, UniformSpace.ball x V s

                                        See also isOpen_iff_open_ball_subset.

                                        theorem nhds_basis_uniformity' {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ιProp} {s : ιSet (α × α)} (h : (uniformity α).HasBasis p s) {x : α} :
                                        (nhds x).HasBasis p fun (i : ι) => UniformSpace.ball x (s i)
                                        theorem nhds_basis_uniformity {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ιProp} {s : ιSet (α × α)} (h : (uniformity α).HasBasis p s) {x : α} :
                                        (nhds x).HasBasis p fun (i : ι) => {y : α | (y, x) s i}
                                        theorem nhds_eq_comap_uniformity' {α : Type ua} [UniformSpace α] {x : α} :
                                        nhds x = Filter.comap (fun (y : α) => (y, x)) (uniformity α)
                                        theorem UniformSpace.mem_nhds_iff {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
                                        s nhds x Vuniformity α, UniformSpace.ball x V s
                                        theorem UniformSpace.ball_mem_nhds {α : Type ua} [UniformSpace α] (x : α) ⦃V : Set (α × α) (V_in : V uniformity α) :
                                        theorem UniformSpace.ball_mem_nhdsWithin {α : Type ua} [UniformSpace α] {x : α} {S : Set α} ⦃V : Set (α × α) (x_in : x S) (V_in : V uniformity α Filter.principal (S ×ˢ S)) :
                                        theorem UniformSpace.mem_nhds_iff_symm {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
                                        theorem UniformSpace.hasBasis_nhds {α : Type ua} [UniformSpace α] (x : α) :
                                        (nhds x).HasBasis (fun (s : Set (α × α)) => s uniformity α SymmetricRel s) fun (s : Set (α × α)) => UniformSpace.ball x s
                                        theorem UniformSpace.mem_closure_iff_symm_ball {α : Type ua} [UniformSpace α] {s : Set α} {x : α} :
                                        x closure s ∀ {V : Set (α × α)}, V uniformity αSymmetricRel V(s UniformSpace.ball x V).Nonempty
                                        theorem UniformSpace.mem_closure_iff_ball {α : Type ua} [UniformSpace α] {s : Set α} {x : α} :
                                        x closure s ∀ {V : Set (α × α)}, V uniformity α(UniformSpace.ball x V s).Nonempty
                                        theorem UniformSpace.hasBasis_nhds_prod {α : Type ua} [UniformSpace α] (x : α) (y : α) :
                                        (nhds (x, y)).HasBasis (fun (s : Set (α × α)) => s uniformity α SymmetricRel s) fun (s : Set (α × α)) => UniformSpace.ball x s ×ˢ UniformSpace.ball y s
                                        theorem nhds_eq_uniformity {α : Type ua} [UniformSpace α] {x : α} :
                                        theorem nhds_eq_uniformity' {α : Type ua} [UniformSpace α] {x : α} :
                                        nhds x = (uniformity α).lift' fun (s : Set (α × α)) => {y : α | (y, x) s}
                                        theorem mem_nhds_left {α : Type ua} [UniformSpace α] (x : α) {s : Set (α × α)} (h : s uniformity α) :
                                        {y : α | (x, y) s} nhds x
                                        theorem mem_nhds_right {α : Type ua} [UniformSpace α] (y : α) {s : Set (α × α)} (h : s uniformity α) :
                                        {x : α | (x, y) s} nhds y
                                        theorem exists_mem_nhds_ball_subset_of_mem_nhds {α : Type ua} [UniformSpace α] {a : α} {U : Set α} (h : U nhds a) :
                                        Vnhds a, tuniformity α, a'V, UniformSpace.ball a' t U
                                        theorem tendsto_right_nhds_uniformity {α : Type ua} [UniformSpace α] {a : α} :
                                        Filter.Tendsto (fun (a' : α) => (a', a)) (nhds a) (uniformity α)
                                        theorem tendsto_left_nhds_uniformity {α : Type ua} [UniformSpace α] {a : α} :
                                        Filter.Tendsto (fun (a' : α) => (a, a')) (nhds a) (uniformity α)
                                        theorem lift_nhds_left {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set αFilter β} (hg : Monotone g) :
                                        (nhds x).lift g = (uniformity α).lift fun (s : Set (α × α)) => g (UniformSpace.ball x s)
                                        theorem lift_nhds_right {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set αFilter β} (hg : Monotone g) :
                                        (nhds x).lift g = (uniformity α).lift fun (s : Set (α × α)) => g {y : α | (y, x) s}
                                        theorem nhds_nhds_eq_uniformity_uniformity_prod {α : Type ua} [UniformSpace α] {a : α} {b : α} :
                                        nhds a ×ˢ nhds b = (uniformity α).lift fun (s : Set (α × α)) => (uniformity α).lift' fun (t : Set (α × α)) => {y : α | (y, a) s} ×ˢ {y : α | (b, y) t}
                                        theorem nhds_eq_uniformity_prod {α : Type ua} [UniformSpace α] {a : α} {b : α} :
                                        nhds (a, b) = (uniformity α).lift' fun (s : Set (α × α)) => {y : α | (y, a) s} ×ˢ {y : α | (b, y) s}
                                        theorem nhdset_of_mem_uniformity {α : Type ua} [UniformSpace α] {d : Set (α × α)} (s : Set (α × α)) (hd : d uniformity α) :
                                        ∃ (t : Set (α × α)), IsOpen t s t t {p : α × α | ∃ (x : α) (y : α), (p.1, x) d (x, y) s (y, p.2) d}
                                        theorem nhds_le_uniformity {α : Type ua} [UniformSpace α] (x : α) :
                                        nhds (x, x) uniformity α

                                        Entourages are neighborhoods of the diagonal.

                                        theorem iSup_nhds_le_uniformity {α : Type ua} [UniformSpace α] :
                                        ⨆ (x : α), nhds (x, x) uniformity α

                                        Entourages are neighborhoods of the diagonal.

                                        Entourages are neighborhoods of the diagonal.

                                        Closure and interior in uniform spaces #

                                        theorem closure_eq_uniformity {α : Type ua} [UniformSpace α] (s : Set (α × α)) :
                                        closure s = V{V : Set (α × α) | V uniformity α SymmetricRel V}, compRel (compRel V s) V
                                        theorem uniformity_hasBasis_closed {α : Type ua} [UniformSpace α] :
                                        (uniformity α).HasBasis (fun (V : Set (α × α)) => V uniformity α IsClosed V) id
                                        theorem uniformity_eq_uniformity_closure {α : Type ua} [UniformSpace α] :
                                        uniformity α = (uniformity α).lift' closure
                                        theorem Filter.HasBasis.uniformity_closure {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ιProp} {U : ιSet (α × α)} (h : (uniformity α).HasBasis p U) :
                                        (uniformity α).HasBasis p fun (i : ι) => closure (U i)
                                        theorem uniformity_hasBasis_closure {α : Type ua} [UniformSpace α] :
                                        (uniformity α).HasBasis (fun (V : Set (α × α)) => V uniformity α) closure

                                        Closed entourages form a basis of the uniformity filter.

                                        theorem closure_eq_inter_uniformity {α : Type ua} [UniformSpace α] {t : Set (α × α)} :
                                        closure t = duniformity α, compRel d (compRel t d)
                                        theorem uniformity_eq_uniformity_interior {α : Type ua} [UniformSpace α] :
                                        uniformity α = (uniformity α).lift' interior
                                        theorem interior_mem_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                        theorem mem_uniformity_isClosed {α : Type ua} [UniformSpace α] {s : Set (α × α)} (h : s uniformity α) :
                                        tuniformity α, IsClosed t t s
                                        theorem isOpen_iff_open_ball_subset {α : Type ua} [UniformSpace α] {s : Set α} :
                                        IsOpen s xs, Vuniformity α, IsOpen V UniformSpace.ball x V s
                                        theorem Dense.biUnion_uniformity_ball {α : Type ua} [UniformSpace α] {s : Set α} {U : Set (α × α)} (hs : Dense s) (hU : U uniformity α) :
                                        xs, UniformSpace.ball x U = Set.univ

                                        The uniform neighborhoods of all points of a dense set cover the whole space.

                                        theorem DenseRange.iUnion_uniformity_ball {α : Type ua} [UniformSpace α] {ι : Type u_2} {xs : ια} (xs_dense : DenseRange xs) {U : Set (α × α)} (hU : U uniformity α) :
                                        ⋃ (i : ι), UniformSpace.ball (xs i) U = Set.univ

                                        The uniform neighborhoods of all points of a dense indexed collection cover the whole space.

                                        Uniformity bases #

                                        theorem uniformity_hasBasis_open {α : Type ua} [UniformSpace α] :
                                        (uniformity α).HasBasis (fun (V : Set (α × α)) => V uniformity α IsOpen V) id

                                        Open elements of 𝓤 α form a basis of 𝓤 α.

                                        theorem Filter.HasBasis.mem_uniformity_iff {α : Type ua} {β : Type ub} [UniformSpace α] {p : βProp} {s : βSet (α × α)} (h : (uniformity α).HasBasis p s) {t : Set (α × α)} :
                                        t uniformity α ∃ (i : β), p i ∀ (a b : α), (a, b) s i(a, b) t
                                        theorem uniformity_hasBasis_open_symmetric {α : Type ua} [UniformSpace α] :
                                        (uniformity α).HasBasis (fun (V : Set (α × α)) => V uniformity α IsOpen V SymmetricRel V) id

                                        Open elements s : Set (α × α) of 𝓤 α such that (x, y) ∈ s ↔ (y, x) ∈ s form a basis of 𝓤 α.

                                        theorem comp_open_symm_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s uniformity α) :
                                        tuniformity α, IsOpen t SymmetricRel t compRel t t s
                                        theorem UniformSpace.has_seq_basis (α : Type ua) [UniformSpace α] [(uniformity α).IsCountablyGenerated] :
                                        ∃ (V : Set (α × α)), (uniformity α).HasAntitoneBasis V ∀ (n : ), SymmetricRel (V n)
                                        theorem Filter.HasBasis.biInter_biUnion_ball {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ιProp} {U : ιSet (α × α)} (h : (uniformity α).HasBasis p U) (s : Set α) :
                                        ⋂ (i : ι), ⋂ (_ : p i), xs, UniformSpace.ball x (U i) = closure s

                                        Uniform continuity #

                                        def UniformContinuous {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] (f : αβ) :

                                        A function f : α → β is uniformly continuous if (f x, f y) tends to the diagonal as (x, y) tends to the diagonal. In other words, if x is sufficiently close to y, then f x is close to f y no matter where x and y are located in α.

                                        Equations
                                        Instances For

                                          Notation for uniform continuity with respect to non-standard UniformSpace instances.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def UniformContinuousOn {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] (f : αβ) (s : Set α) :

                                            A function f : α → β is uniformly continuous on s : Set α if (f x, f y) tends to the diagonal as (x, y) tends to the diagonal while remaining in s ×ˢ s. In other words, if x is sufficiently close to y, then f x is close to f y no matter where x and y are located in s.

                                            Equations
                                            Instances For
                                              theorem uniformContinuous_def {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} :
                                              UniformContinuous f runiformity β, {x : α × α | (f x.1, f x.2) r} uniformity α
                                              theorem uniformContinuous_iff_eventually {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} :
                                              UniformContinuous f runiformity β, ∀ᶠ (x : α × α) in uniformity α, (f x.1, f x.2) r
                                              theorem uniformContinuousOn_univ {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} :
                                              theorem uniformContinuous_of_const {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {c : αβ} (h : ∀ (a b : α), c a = c b) :
                                              theorem uniformContinuous_const {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {b : β} :
                                              UniformContinuous fun (x : α) => b
                                              theorem UniformContinuous.comp {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {g : βγ} {f : αβ} (hg : UniformContinuous g) (hf : UniformContinuous f) :
                                              theorem UniformContinuous.iterate {β : Type ub} [UniformSpace β] (T : ββ) (n : ) (h : UniformContinuous T) :

                                              If a function T is uniformly continuous in a uniform space β, then its n-th iterate T^[n] is also uniformly continuous.

                                              theorem Filter.HasBasis.uniformContinuous_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] {ι' : Sort u_2} [UniformSpace β] {p : ιProp} {s : ιSet (α × α)} (ha : (uniformity α).HasBasis p s) {q : ι'Prop} {t : ι'Set (β × β)} (hb : (uniformity β).HasBasis q t) {f : αβ} :
                                              UniformContinuous f ∀ (i : ι'), q i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) t i
                                              theorem Filter.HasBasis.uniformContinuousOn_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] {ι' : Sort u_2} [UniformSpace β] {p : ιProp} {s : ιSet (α × α)} (ha : (uniformity α).HasBasis p s) {q : ι'Prop} {t : ι'Set (β × β)} (hb : (uniformity β).HasBasis q t) {f : αβ} {S : Set α} :
                                              UniformContinuousOn f S ∀ (i : ι'), q i∃ (j : ι), p j xS, yS, (x, y) s j(f x, f y) t i
                                              Equations
                                              theorem UniformSpace.le_def {α : Type ua} {u₁ : UniformSpace α} {u₂ : UniformSpace α} :
                                              u₁ u₂ uniformity α uniformity α
                                              Equations
                                              theorem UniformSpace.sInf_le {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α} (h : t tt) :
                                              sInf tt t
                                              theorem UniformSpace.le_sInf {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α} (h : t'tt, t t') :
                                              t sInf tt
                                              instance instTopUniformSpace {α : Type ua} :
                                              Equations
                                              instance instBotUniformSpace {α : Type ua} :
                                              Equations
                                              instance instInfUniformSpace {α : Type ua} :
                                              Equations
                                              Equations
                                              theorem iInf_uniformity {α : Type ua} {ι : Sort u_2} {u : ιUniformSpace α} :
                                              uniformity α = ⨅ (i : ι), uniformity α
                                              theorem top_uniformity {α : Type ua} :
                                              Equations
                                              • inhabitedUniformSpace = { default := }
                                              Equations
                                              • inhabitedUniformSpaceCore = { default := default.toCore }
                                              Equations
                                              • instUniqueUniformSpaceOfSubsingleton = { toInhabited := inhabitedUniformSpace, uniq := }
                                              @[reducible, inline]
                                              abbrev UniformSpace.comap {α : Type ua} {β : Type ub} (f : αβ) (u : UniformSpace β) :

                                              Given f : α → β and a uniformity u on β, the inverse image of u under f is the inverse image in the filter sense of the induced function α × α → β × β. See note [reducible non-instances].

                                              Equations
                                              Instances For
                                                theorem uniformity_comap {α : Type ua} {β : Type ub} :
                                                ∀ {x : UniformSpace β} (f : αβ), uniformity α = Filter.comap (Prod.map f f) (uniformity β)
                                                theorem ball_preimage {α : Type ua} {β : Type ub} {f : αβ} {U : Set (β × β)} {x : α} :
                                                @[simp]
                                                theorem UniformSpace.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} {uγ : UniformSpace γ} {f : αβ} {g : βγ} :
                                                theorem UniformSpace.comap_inf {α : Type u_2} {γ : Type u_3} {u₁ : UniformSpace γ} {u₂ : UniformSpace γ} {f : αγ} :
                                                theorem UniformSpace.comap_iInf {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ιUniformSpace γ} {f : αγ} :
                                                UniformSpace.comap f (⨅ (i : ι), u i) = ⨅ (i : ι), UniformSpace.comap f (u i)
                                                theorem UniformSpace.comap_mono {α : Type u_2} {γ : Type u_3} {f : αγ} :
                                                theorem uniformContinuous_iff {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : αβ} :
                                                theorem uniformContinuous_comap {α : Type ua} {β : Type ub} {f : αβ} [u : UniformSpace β] :
                                                theorem uniformContinuous_comap' {α : Type ua} {β : Type ub} {γ : Type uc} {f : γβ} {g : αγ} [v : UniformSpace β] [u : UniformSpace α] (h : UniformContinuous (f g)) :
                                                theorem UniformSpace.to_nhds_mono {α : Type ua} {u₁ : UniformSpace α} {u₂ : UniformSpace α} (h : u₁ u₂) (a : α) :
                                                theorem UniformSpace.toTopologicalSpace_mono {α : Type ua} {u₁ : UniformSpace α} {u₂ : UniformSpace α} (h : u₁ u₂) :
                                                UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
                                                theorem UniformSpace.toTopologicalSpace_comap {α : Type ua} {β : Type ub} {f : αβ} {u : UniformSpace β} :
                                                UniformSpace.toTopologicalSpace = TopologicalSpace.induced f UniformSpace.toTopologicalSpace
                                                theorem Filter.HasBasis.uniformSpace_eq_bot {α : Type ua} {ι : Sort u_2} {p : ιProp} {s : ιSet (α × α)} {u : UniformSpace α} (h : (uniformity α).HasBasis p s) :
                                                u = ∃ (i : ι), p i Pairwise fun (x y : α) => (x, y)s i
                                                theorem UniformSpace.toTopologicalSpace_bot {α : Type ua} :
                                                UniformSpace.toTopologicalSpace =
                                                theorem UniformSpace.toTopologicalSpace_top {α : Type ua} :
                                                UniformSpace.toTopologicalSpace =
                                                theorem UniformSpace.toTopologicalSpace_iInf {α : Type ua} {ι : Sort u_2} {u : ιUniformSpace α} :
                                                UniformSpace.toTopologicalSpace = ⨅ (i : ι), UniformSpace.toTopologicalSpace
                                                theorem UniformSpace.toTopologicalSpace_sInf {α : Type ua} {s : Set (UniformSpace α)} :
                                                UniformSpace.toTopologicalSpace = is, UniformSpace.toTopologicalSpace
                                                theorem UniformSpace.toTopologicalSpace_inf {α : Type ua} {u : UniformSpace α} {v : UniformSpace α} :
                                                UniformSpace.toTopologicalSpace = UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
                                                theorem UniformContinuous.continuous {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} (hf : UniformContinuous f) :

                                                Uniform space structure on ULift α.

                                                Equations
                                                theorem UniformContinuous.inf_rng {α : Type ua} {β : Type ub} {f : αβ} {u₁ : UniformSpace α} {u₂ : UniformSpace β} {u₃ : UniformSpace β} (h₁ : UniformContinuous f) (h₂ : UniformContinuous f) :
                                                theorem UniformContinuous.inf_dom_left {α : Type ua} {β : Type ub} {f : αβ} {u₁ : UniformSpace α} {u₂ : UniformSpace α} {u₃ : UniformSpace β} (hf : UniformContinuous f) :
                                                theorem UniformContinuous.inf_dom_right {α : Type ua} {β : Type ub} {f : αβ} {u₁ : UniformSpace α} {u₂ : UniformSpace α} {u₃ : UniformSpace β} (hf : UniformContinuous f) :
                                                theorem uniformContinuous_sInf_dom {α : Type ua} {β : Type ub} {f : αβ} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β} {u : UniformSpace α} (h₁ : u u₁) (hf : UniformContinuous f) :
                                                theorem uniformContinuous_sInf_rng {α : Type ua} {β : Type ub} {f : αβ} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)} :
                                                theorem uniformContinuous_iInf_dom {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : αβ} {u₁ : ιUniformSpace α} {u₂ : UniformSpace β} {i : ι} (hf : UniformContinuous f) :
                                                theorem uniformContinuous_iInf_rng {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : αβ} {u₁ : UniformSpace α} {u₂ : ιUniformSpace β} :

                                                A uniform space with the discrete uniformity has the discrete topology.

                                                Equations
                                                • instUniformSpaceAdditive = inst
                                                Equations
                                                • instUniformSpaceMultiplicative = inst
                                                theorem uniformContinuous_ofMul {α : Type ua} [UniformSpace α] :
                                                UniformContinuous Additive.ofMul
                                                theorem uniformContinuous_toMul {α : Type ua} [UniformSpace α] :
                                                UniformContinuous Additive.toMul
                                                theorem uniformContinuous_ofAdd {α : Type ua} [UniformSpace α] :
                                                UniformContinuous Multiplicative.ofAdd
                                                theorem uniformContinuous_toAdd {α : Type ua} [UniformSpace α] :
                                                UniformContinuous Multiplicative.toAdd
                                                theorem uniformity_additive {α : Type ua} [UniformSpace α] :
                                                uniformity (Additive α) = Filter.map (Prod.map Additive.ofMul Additive.ofMul) (uniformity α)
                                                theorem uniformity_multiplicative {α : Type ua} [UniformSpace α] :
                                                uniformity (Multiplicative α) = Filter.map (Prod.map Multiplicative.ofAdd Multiplicative.ofAdd) (uniformity α)
                                                instance instUniformSpaceSubtype {α : Type ua} {p : αProp} [t : UniformSpace α] :
                                                Equations
                                                theorem uniformity_subtype {α : Type ua} {p : αProp} [UniformSpace α] :
                                                uniformity (Subtype p) = Filter.comap (fun (q : Subtype p × Subtype p) => (q.1, q.2)) (uniformity α)
                                                theorem uniformity_setCoe {α : Type ua} {s : Set α} [UniformSpace α] :
                                                uniformity s = Filter.comap (Prod.map Subtype.val Subtype.val) (uniformity α)
                                                theorem map_uniformity_set_coe {α : Type ua} {s : Set α} [UniformSpace α] :
                                                Filter.map (Prod.map Subtype.val Subtype.val) (uniformity s) = uniformity α Filter.principal (s ×ˢ s)
                                                theorem uniformContinuous_subtype_val {α : Type ua} {p : αProp} [UniformSpace α] :
                                                UniformContinuous Subtype.val
                                                theorem UniformContinuous.subtype_mk {α : Type ua} {β : Type ub} {p : αProp} [UniformSpace α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (h : ∀ (x : β), p (f x)) :
                                                UniformContinuous fun (x : β) => f x,
                                                theorem uniformContinuousOn_iff_restrict {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} {s : Set α} :
                                                theorem tendsto_of_uniformContinuous_subtype {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} {s : Set α} {a : α} (hf : UniformContinuous fun (x : s) => f x) (ha : s nhds a) :
                                                Filter.Tendsto f (nhds a) (nhds (f a))
                                                theorem UniformContinuousOn.continuousOn {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : αβ} {s : Set α} (h : UniformContinuousOn f s) :
                                                Equations
                                                Equations
                                                instance instUniformSpaceProd {α : Type ua} {β : Type ub} [u₁ : UniformSpace α] [u₂ : UniformSpace β] :
                                                Equations
                                                theorem uniformity_prod {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                uniformity (α × β) = Filter.comap (fun (p : (α × β) × α × β) => (p.1.1, p.2.1)) (uniformity α) Filter.comap (fun (p : (α × β) × α × β) => (p.1.2, p.2.2)) (uniformity β)
                                                instance instIsCountablyGeneratedProdUniformity {α : Type ua} {β : Type ub} [UniformSpace α] [(uniformity α).IsCountablyGenerated] [UniformSpace β] [(uniformity β).IsCountablyGenerated] :
                                                (uniformity (α × β)).IsCountablyGenerated
                                                Equations
                                                • =
                                                theorem uniformity_prod_eq_comap_prod {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                uniformity (α × β) = Filter.comap (fun (p : (α × β) × α × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)
                                                theorem uniformity_prod_eq_prod {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                uniformity (α × β) = Filter.map (fun (p : (α × α) × β × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)
                                                theorem mem_uniformity_of_uniformContinuous_invariant {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {s : Set (β × β)} {f : ααβ} (hf : UniformContinuous fun (p : α × α) => f p.1 p.2) (hs : s uniformity β) :
                                                uuniformity α, ∀ (a b c : α), (a, b) u(f a c, f b c) s
                                                def entourageProd {α : Type ua} {β : Type ub} (u : Set (α × α)) (v : Set (β × β)) :
                                                Set ((α × β) × α × β)

                                                An entourage of the diagonal in α and an entourage in β yield an entourage in α × β once we permute coordinates.

                                                Equations
                                                Instances For
                                                  theorem mem_entourageProd {α : Type ua} {β : Type ub} {u : Set (α × α)} {v : Set (β × β)} {p : (α × β) × α × β} :
                                                  p entourageProd u v (p.1.1, p.2.1) u (p.1.2, p.2.2) v
                                                  theorem entourageProd_mem_uniformity {α : Type ua} {β : Type ub} [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : Set (α × α)} {v : Set (β × β)} (hu : u uniformity α) (hv : v uniformity β) :
                                                  theorem ball_entourageProd {α : Type ua} {β : Type ub} (u : Set (α × α)) (v : Set (β × β)) (x : α × β) :
                                                  theorem Filter.HasBasis.uniformity_prod {α : Type ua} {β : Type ub} {ιa : Type u_2} {ιb : Type u_3} [UniformSpace α] [UniformSpace β] {pa : ιaProp} {pb : ιbProp} {sa : ιaSet (α × α)} {sb : ιbSet (β × β)} (ha : (uniformity α).HasBasis pa sa) (hb : (uniformity β).HasBasis pb sb) :
                                                  (uniformity (α × β)).HasBasis (fun (i : ιa × ιb) => pa i.1 pb i.2) fun (i : ιa × ιb) => entourageProd (sa i.1) (sb i.2)
                                                  theorem entourageProd_subset {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {s : Set ((α × β) × α × β)} (h : s uniformity (α × β)) :
                                                  uuniformity α, vuniformity β, entourageProd u v s
                                                  theorem tendsto_prod_uniformity_fst {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                  Filter.Tendsto (fun (p : (α × β) × α × β) => (p.1.1, p.2.1)) (uniformity (α × β)) (uniformity α)
                                                  theorem tendsto_prod_uniformity_snd {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                  Filter.Tendsto (fun (p : (α × β) × α × β) => (p.1.2, p.2.2)) (uniformity (α × β)) (uniformity β)
                                                  theorem uniformContinuous_fst {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                  UniformContinuous fun (p : α × β) => p.1
                                                  theorem uniformContinuous_snd {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                  UniformContinuous fun (p : α × β) => p.2
                                                  theorem UniformContinuous.prod_mk {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f₁ : αβ} {f₂ : αγ} (h₁ : UniformContinuous f₁) (h₂ : UniformContinuous f₂) :
                                                  UniformContinuous fun (a : α) => (f₁ a, f₂ a)
                                                  theorem UniformContinuous.prod_mk_left {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α × βγ} (h : UniformContinuous f) (b : β) :
                                                  UniformContinuous fun (a : α) => f (a, b)
                                                  theorem UniformContinuous.prod_mk_right {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α × βγ} (h : UniformContinuous f) (a : α) :
                                                  UniformContinuous fun (b : β) => f (a, b)
                                                  theorem UniformContinuous.prod_map {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] {f : αγ} {g : βδ} (hf : UniformContinuous f) (hg : UniformContinuous g) :
                                                  theorem toTopologicalSpace_prod {α : Type u_2} {β : Type u_3} [u : UniformSpace α] [v : UniformSpace β] :
                                                  UniformSpace.toTopologicalSpace = instTopologicalSpaceProd
                                                  theorem uniformContinuous_inf_dom_left₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {ua1 : UniformSpace α} {ua2 : UniformSpace α} {ub1 : UniformSpace β} {ub2 : UniformSpace β} {uc1 : UniformSpace γ} (h : UniformContinuous fun (p : α × β) => f p.1 p.2) :
                                                  UniformContinuous fun (p : α × β) => f p.1 p.2

                                                  A version of UniformContinuous.inf_dom_left for binary functions

                                                  theorem uniformContinuous_inf_dom_right₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {ua1 : UniformSpace α} {ua2 : UniformSpace α} {ub1 : UniformSpace β} {ub2 : UniformSpace β} {uc1 : UniformSpace γ} (h : UniformContinuous fun (p : α × β) => f p.1 p.2) :
                                                  UniformContinuous fun (p : α × β) => f p.1 p.2

                                                  A version of UniformContinuous.inf_dom_right for binary functions

                                                  theorem uniformContinuous_sInf_dom₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {uas : Set (UniformSpace α)} {ubs : Set (UniformSpace β)} {ua : UniformSpace α} {ub : UniformSpace β} {uc : UniformSpace γ} (ha : ua uas) (hb : ub ubs) (hf : UniformContinuous fun (p : α × β) => f p.1 p.2) :
                                                  UniformContinuous fun (p : α × β) => f p.1 p.2

                                                  A version of uniformContinuous_sInf_dom for binary functions

                                                  def UniformContinuous₂ {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (f : αβγ) :

                                                  Uniform continuity for functions of two variables.

                                                  Equations
                                                  Instances For
                                                    theorem uniformContinuous₂_def {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (f : αβγ) :
                                                    theorem UniformContinuous₂.uniformContinuous {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : αβγ} (h : UniformContinuous₂ f) :
                                                    theorem UniformContinuous₂.comp {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] {f : αβγ} {g : γδ} (hg : UniformContinuous g) (hf : UniformContinuous₂ f) :
                                                    theorem UniformContinuous₂.bicompl {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} {δ' : Type u_2} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] [UniformSpace δ'] {f : αβγ} {ga : δα} {gb : δ'β} (hf : UniformContinuous₂ f) (hga : UniformContinuous ga) (hgb : UniformContinuous gb) :
                                                    theorem toTopologicalSpace_subtype {α : Type ua} [u : UniformSpace α] {p : αProp} :
                                                    UniformSpace.toTopologicalSpace = instTopologicalSpaceSubtype
                                                    instance Sum.instUniformSpace {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :

                                                    Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained by taking independently an entourage of the diagonal in the first part, and an entourage of the diagonal in the second part.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    @[reducible, deprecated Sum.instUniformSpace]
                                                    def Sum.uniformSpace {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :

                                                    Alias of Sum.instUniformSpace.


                                                    Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained by taking independently an entourage of the diagonal in the first part, and an entourage of the diagonal in the second part.

                                                    Equations
                                                    Instances For
                                                      theorem union_mem_uniformity_sum {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {a : Set (α × α)} (ha : a uniformity α) {b : Set (β × β)} (hb : b uniformity β) :
                                                      Prod.map Sum.inl Sum.inl '' a Prod.map Sum.inr Sum.inr '' b uniformity (α β)

                                                      The union of an entourage of the diagonal in each set of a disjoint union is again an entourage of the diagonal.

                                                      theorem Sum.uniformity {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                      uniformity (α β) = Filter.map (Prod.map Sum.inl Sum.inl) (uniformity α) Filter.map (Prod.map Sum.inr Sum.inr) (uniformity β)
                                                      theorem uniformContinuous_inl {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                      theorem uniformContinuous_inr {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] :
                                                      instance instIsCountablyGeneratedProdSumUniformity {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] [(uniformity α).IsCountablyGenerated] [(uniformity β).IsCountablyGenerated] :
                                                      (uniformity (α β)).IsCountablyGenerated
                                                      Equations
                                                      • =

                                                      Compact sets in uniform spaces #

                                                      theorem lebesgue_number_lemma {α : Type ua} [UniformSpace α] {K : Set α} {ι : Sort u_2} {U : ιSet α} (hK : IsCompact K) (hopen : ∀ (i : ι), IsOpen (U i)) (hcover : K ⋃ (i : ι), U i) :
                                                      Vuniformity α, xK, ∃ (i : ι), UniformSpace.ball x V U i

                                                      Let c : ι → Set α be an open cover of a compact set s. Then there exists an entourage n such that for each x ∈ s its n-neighborhood is contained in some c i.

                                                      theorem Filter.HasBasis.lebesgue_number_lemma {α : Type ua} [UniformSpace α] {K : Set α} {ι' : Sort u_2} {ι : Sort u_3} {p : ι'Prop} {V : ι'Set (α × α)} {U : ιSet α} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) (hopen : ∀ (j : ι), IsOpen (U j)) (hcover : K ⋃ (j : ι), U j) :
                                                      ∃ (i : ι'), p i xK, ∃ (j : ι), UniformSpace.ball x (V i) U j

                                                      Let U : ι → Set α be an open cover of a compact set K. Then there exists an entourage V such that for each x ∈ K its V-neighborhood is included in some U i.

                                                      Moreover, one can choose an entourage from a given basis.

                                                      theorem lebesgue_number_lemma_sUnion {α : Type ua} [UniformSpace α] {K : Set α} {S : Set (Set α)} (hK : IsCompact K) (hopen : sS, IsOpen s) (hcover : K ⋃₀ S) :
                                                      Vuniformity α, xK, sS, UniformSpace.ball x V s

                                                      Let c : Set (Set α) be an open cover of a compact set s. Then there exists an entourage n such that for each x ∈ s its n-neighborhood is contained in some t ∈ c.

                                                      theorem IsCompact.nhdsSet_basis_uniformity {α : Type ua} {ι : Sort u_1} [UniformSpace α] {K : Set α} {p : ιProp} {V : ιSet (α × α)} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) :
                                                      (nhdsSet K).HasBasis p fun (i : ι) => xK, UniformSpace.ball x (V i)

                                                      If K is a compact set in a uniform space and {V i | p i} is a basis of entourages, then {⋃ x ∈ K, UniformSpace.ball x (V i) | p i} is a basis of 𝓝ˢ K.

                                                      Here "{s i | p i} is a basis of a filter l" means Filter.HasBasis l p s.

                                                      theorem Disjoint.exists_uniform_thickening {α : Type ua} [UniformSpace α] {A : Set α} {B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) :
                                                      Vuniformity α, Disjoint (⋃ xA, UniformSpace.ball x V) (⋃ xB, UniformSpace.ball x V)
                                                      theorem Disjoint.exists_uniform_thickening_of_basis {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ιProp} {s : ιSet (α × α)} (hU : (uniformity α).HasBasis p s) {A : Set α} {B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) :
                                                      ∃ (i : ι), p i Disjoint (⋃ xA, UniformSpace.ball x (s i)) (⋃ xB, UniformSpace.ball x (s i))
                                                      theorem lebesgue_number_of_compact_open {α : Type ua} [UniformSpace α] {K : Set α} {U : Set α} (hK : IsCompact K) (hU : IsOpen U) (hKU : K U) :
                                                      Vuniformity α, IsOpen V xK, UniformSpace.ball x V U

                                                      A useful consequence of the Lebesgue number lemma: given any compact set K contained in an open set U, we can find an (open) entourage V such that the ball of size V about any point of K is contained in U.

                                                      Expressing continuity properties in uniform spaces #

                                                      We reformulate the various continuity properties of functions taking values in a uniform space in terms of the uniformity in the target. Since the same lemmas (essentially with the same names) also exist for metric spaces and emetric spaces (reformulating things in terms of the distance or the edistance in the target), we put them in a namespace Uniform here.

                                                      In the metric and emetric space setting, there are also similar lemmas where one assumes that both the source and the target are metric spaces, reformulating things in terms of the distance on both sides. These lemmas are generally written without primes, and the versions where only the target is a metric space is primed. We follow the same convention here, thus giving lemmas with primes.

                                                      theorem Uniform.tendsto_nhds_right {α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : βα} {a : α} :
                                                      Filter.Tendsto u f (nhds a) Filter.Tendsto (fun (x : β) => (a, u x)) f (uniformity α)
                                                      theorem Uniform.tendsto_nhds_left {α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : βα} {a : α} :
                                                      Filter.Tendsto u f (nhds a) Filter.Tendsto (fun (x : β) => (u x, a)) f (uniformity α)
                                                      theorem Uniform.continuousAt_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {b : β} :
                                                      ContinuousAt f b Filter.Tendsto (fun (x : β) => (f b, f x)) (nhds b) (uniformity α)
                                                      theorem Uniform.continuousAt_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {b : β} :
                                                      ContinuousAt f b Filter.Tendsto (fun (x : β) => (f x, f b)) (nhds b) (uniformity α)
                                                      theorem Uniform.continuousAt_iff_prod {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {b : β} :
                                                      ContinuousAt f b Filter.Tendsto (fun (x : β × β) => (f x.1, f x.2)) (nhds (b, b)) (uniformity α)
                                                      theorem Uniform.continuousWithinAt_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {b : β} {s : Set β} :
                                                      ContinuousWithinAt f s b Filter.Tendsto (fun (x : β) => (f b, f x)) (nhdsWithin b s) (uniformity α)
                                                      theorem Uniform.continuousWithinAt_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {b : β} {s : Set β} :
                                                      ContinuousWithinAt f s b Filter.Tendsto (fun (x : β) => (f x, f b)) (nhdsWithin b s) (uniformity α)
                                                      theorem Uniform.continuousOn_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {s : Set β} :
                                                      ContinuousOn f s bs, Filter.Tendsto (fun (x : β) => (f b, f x)) (nhdsWithin b s) (uniformity α)
                                                      theorem Uniform.continuousOn_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} {s : Set β} :
                                                      ContinuousOn f s bs, Filter.Tendsto (fun (x : β) => (f x, f b)) (nhdsWithin b s) (uniformity α)
                                                      theorem Uniform.continuous_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} :
                                                      Continuous f ∀ (b : β), Filter.Tendsto (fun (x : β) => (f b, f x)) (nhds b) (uniformity α)
                                                      theorem Uniform.continuous_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : βα} :
                                                      Continuous f ∀ (b : β), Filter.Tendsto (fun (x : β) => (f x, f b)) (nhds b) (uniformity α)
                                                      theorem Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {r : Set (α × α)} {s : Set β} {f : βα} {g : βα} (hf : xs, ContinuousAt f x) (hg : xs, ContinuousAt g x) (hfg : Set.EqOn f g s) (hr : r uniformity α) :
                                                      ∃ (t : Set β), IsOpen t s t xt, (f x, g x) r

                                                      Consider two functions f and g which coincide on a set s and are continuous there. Then there is an open neighborhood of s on which f and g are uniformly close.

                                                      theorem Filter.Tendsto.congr_uniformity {α : Type u_2} {β : Type u_3} [UniformSpace β] {f : αβ} {g : αβ} {l : Filter α} {b : β} (hf : Filter.Tendsto f l (nhds b)) (hg : Filter.Tendsto (fun (x : α) => (f x, g x)) l (uniformity β)) :
                                                      theorem Uniform.tendsto_congr {α : Type u_2} {β : Type u_3} [UniformSpace β] {f : αβ} {g : αβ} {l : Filter α} {b : β} (hfg : Filter.Tendsto (fun (x : α) => (f x, g x)) l (uniformity β)) :