mathlib3 documentation

topology.uniform_space.basic

Uniform spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 := (λ 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 uniform_space X of uniform structures on X, as well as the pullback (uniform_space.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 uniform_space 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 id_rel {α : Type u_1} :
set × α)

The identity relation, or the graph of the identity function

Equations
@[simp]
theorem mem_id_rel {α : Type u_1} {a b : α} :
(a, b) id_rel a = b
@[simp]
theorem id_rel_subset {α : Type u_1} {s : set × α)} :
id_rel s (a : α), (a, a) s
def comp_rel {α : Type u} (r₁ r₂ : set × α)) :
set × α)

The composition of relations

Equations
@[simp]
theorem mem_comp_rel {α : Type u_1} {r₁ r₂ : set × α)} {x y : α} :
(x, y) comp_rel r₁ r₂ (z : α), (x, z) r₁ (z, y) r₂
@[simp]
theorem swap_id_rel {α : Type u_1} :
theorem monotone.comp_rel {α : Type u_1} {β : Type u_2} [preorder β] {f g : β set × α)} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), comp_rel (f x) (g x))
theorem comp_rel_mono {α : Type u_1} {f g h k : set × α)} (h₁ : f h) (h₂ : g k) :
theorem prod_mk_mem_comp_rel {α : Type u_1} {a b c : α} {s t : set × α)} (h₁ : (a, c) s) (h₂ : (c, b) t) :
(a, b) comp_rel s t
@[simp]
theorem id_comp_rel {α : Type u_1} {r : set × α)} :
theorem comp_rel_assoc {α : Type u_1} {r s t : set × α)} :
theorem left_subset_comp_rel {α : Type u_1} {s t : set × α)} (h : id_rel t) :
theorem right_subset_comp_rel {α : Type u_1} {s t : set × α)} (h : id_rel s) :
theorem subset_comp_self {α : Type u_1} {s : set × α)} (h : id_rel s) :
theorem subset_iterate_comp_rel {α : Type u_1} {s t : set × α)} (h : id_rel s) (n : ) :
def symmetric_rel {α : Type u_1} (V : set × α)) :
Prop

The relation is invariant under swapping factors.

Equations
def symmetrize_rel {α : Type u_1} (V : set × α)) :
set × α)

The maximal symmetric relation contained in a given relation.

Equations
theorem symmetric_symmetrize_rel {α : Type u_1} (V : set × α)) :
theorem symmetrize_rel_subset_self {α : Type u_1} (V : set × α)) :
theorem symmetrize_mono {α : Type u_1} {V W : set × α)} (h : V W) :
theorem symmetric_rel.mk_mem_comm {α : Type u_1} {V : set × α)} (hV : symmetric_rel V) {x y : α} :
(x, y) V (y, x) V
theorem symmetric_rel.eq {α : Type u_1} {U : set × α)} (hU : symmetric_rel U) :
theorem symmetric_rel.inter {α : Type u_1} {U V : set × α)} (hU : symmetric_rel U) (hV : symmetric_rel V) :
structure uniform_space.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 uniform_space.core
def uniform_space.core.mk' {α : Type u} (U : filter × α)) (refl : (r : set × α)), r U (x : α), (x, x) r) (symm : (r : set × α)), r U prod.swap ⁻¹' r U) (comp : (r : set × α)), r U ( (t : set × α)) (H : t U), comp_rel t t r)) :

An alternative constructor for uniform_space.core. This version unfolds various filter-related definitions.

Equations
def uniform_space.core.mk_of_basis {α : Type u} (B : filter_basis × α)) (refl : (r : set × α)), r B (x : α), (x, x) r) (symm : (r : set × α)), r B ( (t : set × α)) (H : t B), t prod.swap ⁻¹' r)) (comp : (r : set × α)), r B ( (t : set × α)) (H : t B), comp_rel t t r)) :

Defining an uniform_space.core from a filter basis satisfying some uniformity-like axioms.

Equations

A uniform space generates a topological space

Equations
theorem uniform_space.core_eq {α : Type u_1} {u₁ u₂ : uniform_space.core α} :
u₁.uniformity = u₂.uniformity u₁ = u₂
@[class]
structure uniform_space (α : Type u) :

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 of this typeclass
Instances of other typeclasses for uniform_space
def uniform_space.mk' {α : Type u_1} (t : topological_space α) (c : uniform_space.core α) (is_open_uniformity : (s : set α), is_open s (x : α), x s {p : α × α | p.fst = x p.snd s} c.uniformity) :

Alternative constructor for uniform_space α when a topology is already given.

Equations

Construct a uniform_space from a u : uniform_space.core and a topological_space structure that is equal to u.to_topological_space.

Equations
def uniformity (α : Type u) [uniform_space α] :
filter × α)

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

Equations
Instances for uniformity
@[ext]
theorem uniform_space_eq {α : Type u_1} {u₁ u₂ : uniform_space α} :
uniformity α = uniformity α u₁ = u₂
@[reducible]

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

Equations
def uniform_space.of_fun {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid β] (d : α α β) (refl : (x : α), d x x = 0) (symm : (x y : α), d x y = d y x) (triangle : (x y z : α), d x z d x y + d y z) (half : (ε : β), ε > 0 ( (δ : β) (H : δ > 0), (x : β), x < δ (y : β), y < δ x + y < ε)) :

Define a uniform_space using a "distance" function. The function can be, e.g., the distance in a (usual or extended) metric space or an absolute value on a ring.

Equations
theorem uniform_space.has_basis_of_fun {α : Type u_1} {β : Type u_2} [linear_ordered_add_comm_monoid β] (h₀ : (x : β), 0 < x) (d : α α β) (refl : (x : α), d x x = 0) (symm : (x y : α), d x y = d y x) (triangle : (x y z : α), d x z d x y + d y z) (half : (ε : β), ε > 0 ( (δ : β) (H : δ > 0), (x : β), x < δ (y : β), y < δ x + y < ε)) :
(uniformity α).has_basis (has_lt.lt 0) (λ (ε : β), {x : α × α | d x.fst x.snd < ε})
theorem is_open_uniformity {α : Type u_1} [uniform_space α] {s : set α} :
is_open s (x : α), x s {p : α × α | p.fst = x p.snd s} uniformity α
@[protected, instance]
def uniformity.ne_bot {α : Type u_1} [uniform_space α] [nonempty α] :
theorem refl_mem_uniformity {α : Type u_1} [uniform_space α] {x : α} {s : set × α)} (h : s uniformity α) :
(x, x) s
theorem mem_uniformity_of_eq {α : Type u_1} [uniform_space α] {x y : α} {s : set × α)} (h : s uniformity α) (hx : x = y) :
(x, y) s
theorem comp_le_uniformity {α : Type u_1} [uniform_space α] :
(uniformity α).lift' (λ (s : set × α)), comp_rel s s) uniformity α
theorem comp_mem_uniformity_sets {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
(t : set × α)) (H : t uniformity α), comp_rel t t s
theorem eventually_uniformity_iterate_comp_subset {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) (n : ) :
∀ᶠ (t : set × α)) in (uniformity α).small_sets, comp_rel t^[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 u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
∀ᶠ (t : set × α)) in (uniformity α).small_sets, comp_rel t t s

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

theorem filter.tendsto.uniformity_trans {α : Type u_1} {β : Type u_2} [uniform_space α] {l : filter β} {f₁ f₂ f₃ : β α} (h₁₂ : filter.tendsto (λ (x : β), (f₁ x, f₂ x)) l (uniformity α)) (h₂₃ : filter.tendsto (λ (x : β), (f₂ x, f₃ x)) l (uniformity α)) :
filter.tendsto (λ (x : β), (f₁ x, f₃ x)) l (uniformity α)

Relation λ f g, tendsto (λ x, (f x, g x)) l (𝓤 α) is transitive.

theorem filter.tendsto.uniformity_symm {α : Type u_1} {β : Type u_2} [uniform_space α] {l : filter β} {f : β α × α} (h : filter.tendsto f l (uniformity α)) :
filter.tendsto (λ (x : β), ((f x).snd, (f x).fst)) l (uniformity α)

Relation λ f g, tendsto (λ x, (f x, g x)) l (𝓤 α) is symmetric

theorem tendsto_diag_uniformity {α : Type u_1} {β : Type u_2} [uniform_space α] (f : β α) (l : filter β) :
filter.tendsto (λ (x : β), (f x, f x)) l (uniformity α)

Relation λ f g, tendsto (λ x, (f x, g x)) l (𝓤 α) is reflexive.

theorem tendsto_const_uniformity {α : Type u_1} {β : Type u_2} [uniform_space α] {a : α} {f : filter β} :
filter.tendsto (λ (_x : β), (a, a)) f (uniformity α)
theorem symm_of_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
(t : set × α)) (H : t uniformity α), ( (a b : α), (a, b) t (b, a) t) t s
theorem comp_symm_of_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
(t : set × α)) (H : t uniformity α), ( {a b : α}, (a, b) t (b, a) t) comp_rel t t s
theorem symmetrize_mem_uniformity {α : Type u_1} [uniform_space α] {V : set × α)} (h : V uniformity α) :
theorem uniform_space.has_basis_symmetric {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (s : set × α)), s uniformity α symmetric_rel s) id

Symmetric entourages form a basis of 𝓤 α

theorem uniformity_lift_le_swap {α : Type u_1} {β : Type u_2} [uniform_space α] {g : set × α) filter β} {f : filter β} (hg : monotone g) (h : (uniformity α).lift (λ (s : set × α)), g (prod.swap ⁻¹' s)) f) :
theorem uniformity_lift_le_comp {α : Type u_1} {β : Type u_2} [uniform_space α] {f : set × α) filter β} (h : monotone f) :
(uniformity α).lift (λ (s : set × α)), f (comp_rel s s)) (uniformity α).lift f
theorem comp_le_uniformity3 {α : Type u_1} [uniform_space α] :
(uniformity α).lift' (λ (s : set × α)), comp_rel s (comp_rel s s)) uniformity α
theorem comp_symm_mem_uniformity_sets {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
(t : set × α)) (H : t uniformity α), symmetric_rel t comp_rel t t s

See also comp_open_symm_mem_uniformity_sets.

theorem subset_comp_self_of_mem_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} (h : s uniformity α) :
theorem comp_comp_symm_mem_uniformity_sets {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
(t : set × α)) (H : t uniformity α), symmetric_rel t comp_rel (comp_rel t t) t s

Balls in uniform spaces #

def uniform_space.ball {β : Type u_2} (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
theorem uniform_space.mem_ball_self {α : Type u_1} [uniform_space α] (x : α) {V : set × α)} (hV : V uniformity α) :
theorem mem_ball_comp {β : Type u_2} {V W : set × β)} {x y z : β} (h : y uniform_space.ball x V) (h' : z uniform_space.ball y W) :

The triangle inequality for uniform_space.ball

theorem ball_subset_of_comp_subset {β : Type u_2} {V W : set × β)} {x y : β} (h : x uniform_space.ball y W) (h' : comp_rel W W V) :
theorem ball_mono {β : Type u_2} {V W : set × β)} (h : V W) (x : β) :
theorem ball_inter {β : Type u_2} (x : β) (V W : set × β)) :
theorem ball_inter_left {β : Type u_2} (x : β) (V W : set × β)) :
theorem ball_inter_right {β : Type u_2} (x : β) (V W : set × β)) :
theorem mem_ball_symmetry {β : Type u_2} {V : set × β)} (hV : symmetric_rel V) {x y : β} :
theorem ball_eq_of_symmetry {β : Type u_2} {V : set × β)} (hV : symmetric_rel V) {x : β} :
uniform_space.ball x V = {y : β | (y, x) V}
theorem mem_comp_of_mem_ball {β : Type u_2} {V W : set × β)} {x y z : β} (hV : symmetric_rel V) (hx : x uniform_space.ball z V) (hy : y uniform_space.ball z W) :
(x, y) comp_rel V W
theorem uniform_space.is_open_ball {α : Type u_1} [uniform_space α] (x : α) {V : set × α)} (hV : is_open V) :
theorem mem_comp_comp {β : Type u_2} {V W M : set × β)} (hW' : symmetric_rel W) {p : β × β} :

Neighborhoods in uniform spaces #

theorem mem_nhds_uniformity_iff_right {α : Type u_1} [uniform_space α] {x : α} {s : set α} :
s nhds x {p : α × α | p.fst = x p.snd s} uniformity α
theorem mem_nhds_uniformity_iff_left {α : Type u_1} [uniform_space α] {x : α} {s : set α} :
s nhds x {p : α × α | p.snd = x p.fst s} uniformity α
theorem nhds_eq_comap_uniformity {α : Type u_1} [uniform_space α] {x : α} :
theorem is_open_iff_ball_subset {α : Type u_1} [uniform_space α] {s : set α} :
is_open s (x : α), x s ( (V : set × α)) (H : V uniformity α), uniform_space.ball x V s)

See also is_open_iff_open_ball_subset.

theorem nhds_basis_uniformity' {α : Type u_1} {ι : Sort u_5} [uniform_space α] {p : ι Prop} {s : ι set × α)} (h : (uniformity α).has_basis p s) {x : α} :
(nhds x).has_basis p (λ (i : ι), uniform_space.ball x (s i))
theorem nhds_basis_uniformity {α : Type u_1} {ι : Sort u_5} [uniform_space α] {p : ι Prop} {s : ι set × α)} (h : (uniformity α).has_basis p s) {x : α} :
(nhds x).has_basis p (λ (i : ι), {y : α | (y, x) s i})
theorem nhds_eq_comap_uniformity' {α : Type u_1} [uniform_space α] {x : α} :
nhds x = filter.comap (λ (y : α), (y, x)) (uniformity α)
theorem uniform_space.mem_nhds_iff {α : Type u_1} [uniform_space α] {x : α} {s : set α} :
s nhds x (V : set × α)) (H : V uniformity α), uniform_space.ball x V s
theorem uniform_space.ball_mem_nhds {α : Type u_1} [uniform_space α] (x : α) ⦃V : set × α) (V_in : V uniformity α) :
theorem uniform_space.mem_nhds_iff_symm {α : Type u_1} [uniform_space α] {x : α} {s : set α} :
s nhds x (V : set × α)) (H : V uniformity α), symmetric_rel V uniform_space.ball x V s
theorem uniform_space.has_basis_nhds {α : Type u_1} [uniform_space α] (x : α) :
(nhds x).has_basis (λ (s : set × α)), s uniformity α symmetric_rel s) (λ (s : set × α)), uniform_space.ball x s)
theorem uniform_space.mem_closure_iff_symm_ball {α : Type u_1} [uniform_space α] {s : set α} {x : α} :
theorem uniform_space.mem_closure_iff_ball {α : Type u_1} [uniform_space α] {s : set α} {x : α} :
theorem uniform_space.has_basis_nhds_prod {α : Type u_1} [uniform_space α] (x y : α) :
(nhds (x, y)).has_basis (λ (s : set × α)), s uniformity α symmetric_rel s) (λ (s : set × α)), uniform_space.ball x s ×ˢ uniform_space.ball y s)
theorem nhds_eq_uniformity {α : Type u_1} [uniform_space α] {x : α} :
theorem nhds_eq_uniformity' {α : Type u_1} [uniform_space α] {x : α} :
nhds x = (uniformity α).lift' (λ (s : set × α)), {y : α | (y, x) s})
theorem mem_nhds_left {α : Type u_1} [uniform_space α] (x : α) {s : set × α)} (h : s uniformity α) :
{y : α | (x, y) s} nhds x
theorem mem_nhds_right {α : Type u_1} [uniform_space α] (y : α) {s : set × α)} (h : s uniformity α) :
{x : α | (x, y) s} nhds y
theorem exists_mem_nhds_ball_subset_of_mem_nhds {α : Type u_1} [uniform_space α] {a : α} {U : set α} (h : U nhds a) :
(V : set α) (H : V nhds a) (t : set × α)) (H : t uniformity α), (a' : α), a' V uniform_space.ball a' t U
theorem is_compact.nhds_set_basis_uniformity {α : Type u_1} {ι : Sort u_5} [uniform_space α] {p : ι Prop} {s : ι set × α)} (hU : (uniformity α).has_basis p s) {K : set α} (hK : is_compact K) :
(nhds_set K).has_basis p (λ (i : ι), (x : α) (H : x K), uniform_space.ball x (s i))
theorem disjoint.exists_uniform_thickening {α : Type u_1} [uniform_space α] {A B : set α} (hA : is_compact A) (hB : is_closed B) (h : disjoint A B) :
(V : set × α)) (H : V uniformity α), disjoint ( (x : α) (H : x A), uniform_space.ball x V) ( (x : α) (H : x B), uniform_space.ball x V)
theorem disjoint.exists_uniform_thickening_of_basis {α : Type u_1} {ι : Sort u_5} [uniform_space α] {p : ι Prop} {s : ι set × α)} (hU : (uniformity α).has_basis p s) {A B : set α} (hA : is_compact A) (hB : is_closed B) (h : disjoint A B) :
(i : ι), p i disjoint ( (x : α) (H : x A), uniform_space.ball x (s i)) ( (x : α) (H : x B), uniform_space.ball x (s i))
theorem tendsto_right_nhds_uniformity {α : Type u_1} [uniform_space α] {a : α} :
filter.tendsto (λ (a' : α), (a', a)) (nhds a) (uniformity α)
theorem tendsto_left_nhds_uniformity {α : Type u_1} [uniform_space α] {a : α} :
filter.tendsto (λ (a' : α), (a, a')) (nhds a) (uniformity α)
theorem lift_nhds_left {α : Type u_1} {β : Type u_2} [uniform_space α] {x : α} {g : set α filter β} (hg : monotone g) :
(nhds x).lift g = (uniformity α).lift (λ (s : set × α)), g (uniform_space.ball x s))
theorem lift_nhds_right {α : Type u_1} {β : Type u_2} [uniform_space α] {x : α} {g : set α filter β} (hg : monotone g) :
(nhds x).lift g = (uniformity α).lift (λ (s : set × α)), g {y : α | (y, x) s})
theorem nhds_nhds_eq_uniformity_uniformity_prod {α : Type u_1} [uniform_space α] {a b : α} :
(nhds a).prod (nhds b) = (uniformity α).lift (λ (s : set × α)), (uniformity α).lift' (λ (t : set × α)), {y : α | (y, a) s} ×ˢ {y : α | (b, y) t}))
theorem nhds_eq_uniformity_prod {α : Type u_1} [uniform_space α] {a b : α} :
nhds (a, b) = (uniformity α).lift' (λ (s : set × α)), {y : α | (y, a) s} ×ˢ {y : α | (b, y) s})
theorem nhdset_of_mem_uniformity {α : Type u_1} [uniform_space α] {d : set × α)} (s : set × α)) (hd : d uniformity α) :
(t : set × α)), is_open t s t t {p : α × α | (x y : α), (p.fst, x) d (x, y) s (y, p.snd) d}
theorem nhds_le_uniformity {α : Type u_1} [uniform_space α] (x : α) :
nhds (x, x) uniformity α

Entourages are neighborhoods of the diagonal.

theorem supr_nhds_le_uniformity {α : Type u_1} [uniform_space α] :
( (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 u_1} [uniform_space α] (s : set × α)) :
closure s = (V : set × α)) (H : V {V : set × α) | V uniformity α symmetric_rel V}), comp_rel (comp_rel V s) V
theorem uniformity_has_basis_closed {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (V : set × α)), V uniformity α is_closed V) id
theorem filter.has_basis.uniformity_closure {α : Type u_1} {ι : Sort u_5} [uniform_space α] {p : ι Prop} {U : ι set × α)} (h : (uniformity α).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), closure (U i))
theorem uniformity_has_basis_closure {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (V : set × α)), V uniformity α) closure

Closed entourages form a basis of the uniformity filter.

theorem closure_eq_inter_uniformity {α : Type u_1} [uniform_space α] {t : set × α)} :
closure t = (d : set × α)) (H : d uniformity α), comp_rel d (comp_rel t d)
theorem interior_mem_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
theorem mem_uniformity_is_closed {α : Type u_1} [uniform_space α] {s : set × α)} (h : s uniformity α) :
(t : set × α)) (H : t uniformity α), is_closed t t s
theorem is_open_iff_open_ball_subset {α : Type u_1} [uniform_space α] {s : set α} :
is_open s (x : α), x s ( (V : set × α)) (H : V uniformity α), is_open V uniform_space.ball x V s)
theorem dense.bUnion_uniformity_ball {α : Type u_1} [uniform_space α] {s : set α} {U : set × α)} (hs : dense s) (hU : U uniformity α) :
( (x : α) (H : x s), uniform_space.ball x U) = set.univ

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

Uniformity bases #

theorem uniformity_has_basis_open {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (V : set × α)), V uniformity α is_open V) id

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

theorem filter.has_basis.mem_uniformity_iff {α : Type u_1} {β : Type u_2} [uniform_space α] {p : β Prop} {s : β set × α)} (h : (uniformity α).has_basis p s) {t : set × α)} :
t uniformity α (i : β) (hi : p i), (a b : α), (a, b) s i (a, b) t

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 u_1} [uniform_space α] {s : set × α)} (hs : s uniformity α) :
(t : set × α)) (H : t uniformity α), is_open t symmetric_rel t comp_rel t t s
theorem filter.has_basis.bInter_bUnion_ball {α : Type u_1} {ι : Sort u_5} [uniform_space α] {p : ι Prop} {U : ι set × α)} (h : (uniformity α).has_basis p U) (s : set α) :
( (i : ι) (hi : p i), (x : α) (H : x s), uniform_space.ball x (U i)) = closure s

Uniform continuity #

def uniform_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α β) :
Prop

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 uniform_continuous
def uniform_continuous_on {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] (f : α β) (s : set α) :
Prop

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
theorem uniform_continuous_def {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} :
uniform_continuous f (r : set × β)), r uniformity β {x : α × α | (f x.fst, f x.snd) r} uniformity α
theorem uniform_continuous_iff_eventually {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} :
uniform_continuous f (r : set × β)), r uniformity β (∀ᶠ (x : α × α) in uniformity α, (f x.fst, f x.snd) r)
theorem uniform_continuous_of_const {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {c : α β} (h : (a b : α), c a = c b) :
theorem uniform_continuous_const {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {b : β} :
uniform_continuous (λ (a : α), b)
theorem uniform_continuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {g : β γ} {f : α β} (hg : uniform_continuous g) (hf : uniform_continuous f) :
theorem filter.has_basis.uniform_continuous_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [uniform_space α] {ι' : Sort u_3} [uniform_space β] {p : ι Prop} {s : ι set × α)} (ha : (uniformity α).has_basis p s) {q : ι' Prop} {t : ι' set × β)} (hb : (uniformity β).has_basis q t) {f : α β} :
uniform_continuous f (i : ι'), q i ( (j : ι) (hj : p j), (x y : α), (x, y) s j (f x, f y) t i)
theorem filter.has_basis.uniform_continuous_on_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [uniform_space α] {ι' : Sort u_3} [uniform_space β] {p : ι Prop} {s : ι set × α)} (ha : (uniformity α).has_basis p s) {q : ι' Prop} {t : ι' set × β)} (hb : (uniformity β).has_basis q t) {f : α β} {S : set α} :
uniform_continuous_on f S (i : ι'), q i ( (j : ι) (hj : p j), (x : α), x S (y : α), y S (x, y) s j (f x, f y) t i)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem infi_uniformity {α : Type u_1} {ι : Sort u_2} {u : ι uniform_space α} :
uniformity α = (i : ι), uniformity α
theorem inf_uniformity {α : Type u_1} {u v : uniform_space α} :
@[protected, instance]
Equations
def uniform_space.comap {α : Type u_1} {β : Type u_2} (f : α β) (u : uniform_space β) :

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 α × α → β × β.

Equations
theorem uniformity_comap {α : Type u_1} {β : Type u_2} [uniform_space β] (f : α β) :
@[simp]
theorem uniform_space.comap_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uγ : uniform_space γ] {f : α β} {g : β γ} :
theorem uniform_space.comap_inf {α : Type u_1} {γ : Type u_2} {u₁ u₂ : uniform_space γ} {f : α γ} :
theorem uniform_space.comap_infi {ι : Sort u_1} {α : Type u_2} {γ : Type u_3} {u : ι uniform_space γ} {f : α γ} :
uniform_space.comap f ( (i : ι), u i) = (i : ι), uniform_space.comap f (u i)
theorem uniform_space.comap_mono {α : Type u_1} {γ : Type u_2} {f : α γ} :
theorem uniform_continuous_iff {α : Type u_1} {β : Type u_2} {uα : uniform_space α} {uβ : uniform_space β} {f : α β} :
theorem uniform_continuous_comap {α : Type u_1} {β : Type u_2} {f : α β} [u : uniform_space β] :
theorem uniform_continuous_comap' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ β} {g : α γ} [v : uniform_space β] [u : uniform_space α] (h : uniform_continuous (f g)) :
theorem to_nhds_mono {α : Type u_1} {u₁ u₂ : uniform_space α} (h : u₁ u₂) (a : α) :
theorem uniform_continuous.continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} (hf : uniform_continuous f) :
@[protected, instance]

Uniform space structure on ulift α.

Equations
theorem uniform_continuous_inf_rng {α : Type u_1} {β : Type u_2} {f : α β} {u₁ : uniform_space α} {u₂ u₃ : uniform_space β} (h₁ : uniform_continuous f) (h₂ : uniform_continuous f) :
theorem uniform_continuous_inf_dom_left {α : Type u_1} {β : Type u_2} {f : α β} {u₁ u₂ : uniform_space α} {u₃ : uniform_space β} (hf : uniform_continuous f) :
theorem uniform_continuous_inf_dom_right {α : Type u_1} {β : Type u_2} {f : α β} {u₁ u₂ : uniform_space α} {u₃ : uniform_space β} (hf : uniform_continuous f) :
theorem uniform_continuous_Inf_dom {α : Type u_1} {β : Type u_2} {f : α β} {u₁ : set (uniform_space α)} {u₂ : uniform_space β} {u : uniform_space α} (h₁ : u u₁) (hf : uniform_continuous f) :
theorem uniform_continuous_Inf_rng {α : Type u_1} {β : Type u_2} {f : α β} {u₁ : uniform_space α} {u₂ : set (uniform_space β)} (h : (u : uniform_space β), u u₂ uniform_continuous f) :
theorem uniform_continuous_infi_dom {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α β} {u₁ : ι uniform_space α} {u₂ : uniform_space β} {i : ι} (hf : uniform_continuous f) :
theorem uniform_continuous_infi_rng {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α β} {u₁ : uniform_space α} {u₂ : ι uniform_space β} (h : (i : ι), uniform_continuous f) :

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def subtype.uniform_space {α : Type u_1} {p : α Prop} [t : uniform_space α] :
Equations
theorem uniformity_subtype {α : Type u_1} {p : α Prop} [t : uniform_space α] :
theorem uniform_continuous.subtype_mk {α : Type u_1} {β : Type u_2} {p : α Prop} [uniform_space α] [uniform_space β] {f : β α} (hf : uniform_continuous f) (h : (x : β), p (f x)) :
uniform_continuous (λ (x : β), f x, _⟩)
theorem uniform_continuous_on_iff_restrict {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} {s : set α} :
theorem tendsto_of_uniform_continuous_subtype {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} {s : set α} {a : α} (hf : uniform_continuous (λ (x : s), f x.val)) (ha : s nhds a) :
filter.tendsto f (nhds a) (nhds (f a))
theorem uniform_continuous_on.continuous_on {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α β} {s : set α} (h : uniform_continuous_on f s) :
@[protected, instance]
def prod.uniform_space {α : Type u_1} {β : Type u_2} [u₁ : uniform_space α] [u₂ : uniform_space β] :
Equations
theorem uniformity_prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniformity × β) = filter.comap (λ (p : × β) × α × β), (p.fst.fst, p.snd.fst)) (uniformity α) filter.comap (λ (p : × β) × α × β), (p.fst.snd, p.snd.snd)) (uniformity β)
theorem uniformity_prod_eq_comap_prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniformity × β) = filter.comap (λ (p : × β) × α × β), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((uniformity α).prod (uniformity β))
theorem uniformity_prod_eq_prod {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniformity × β) = filter.map (λ (p : × α) × β × β), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((uniformity α).prod (uniformity β))
theorem mem_uniformity_of_uniform_continuous_invariant {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set × β)} {f : α α β} (hf : uniform_continuous (λ (p : α × α), f p.fst p.snd)) (hs : s uniformity β) :
(u : set × α)) (H : u uniformity α), (a b c : α), (a, b) u (f a c, f b c) s
theorem mem_uniform_prod {α : Type u_1} {β : Type u_2} [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set × α)} {b : set × β)} (ha : a uniformity α) (hb : b uniformity β) :
{p : × β) × α × β | (p.fst.fst, p.snd.fst) a (p.fst.snd, p.snd.snd) b} uniformity × β)
theorem tendsto_prod_uniformity_fst {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
filter.tendsto (λ (p : × β) × α × β), (p.fst.fst, p.snd.fst)) (uniformity × β)) (uniformity α)
theorem tendsto_prod_uniformity_snd {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
filter.tendsto (λ (p : × β) × α × β), (p.fst.snd, p.snd.snd)) (uniformity × β)) (uniformity β)
theorem uniform_continuous_fst {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniform_continuous (λ (p : α × β), p.fst)
theorem uniform_continuous_snd {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniform_continuous (λ (p : α × β), p.snd)
theorem uniform_continuous.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f₁ : α β} {f₂ : α γ} (h₁ : uniform_continuous f₁) (h₂ : uniform_continuous f₂) :
uniform_continuous (λ (a : α), (f₁ a, f₂ a))
theorem uniform_continuous.prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α × β γ} (h : uniform_continuous f) (b : β) :
uniform_continuous (λ (a : α), f (a, b))
theorem uniform_continuous.prod_mk_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α × β γ} (h : uniform_continuous f) (a : α) :
uniform_continuous (λ (b : β), f (a, b))
theorem uniform_continuous.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] {f : α γ} {g : β δ} (hf : uniform_continuous f) (hg : uniform_continuous g) :
theorem uniform_continuous_inf_dom_left₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {ua1 ua2 : uniform_space α} {ub1 ub2 : uniform_space β} {uc1 : uniform_space γ} (h : uniform_continuous (λ (p : α × β), f p.fst p.snd)) :
uniform_continuous (λ (p : α × β), f p.fst p.snd)

A version of uniform_continuous_inf_dom_left for binary functions

theorem uniform_continuous_inf_dom_right₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {ua1 ua2 : uniform_space α} {ub1 ub2 : uniform_space β} {uc1 : uniform_space γ} (h : uniform_continuous (λ (p : α × β), f p.fst p.snd)) :
uniform_continuous (λ (p : α × β), f p.fst p.snd)

A version of uniform_continuous_inf_dom_right for binary functions

theorem uniform_continuous_Inf_dom₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {uas : set (uniform_space α)} {ubs : set (uniform_space β)} {ua : uniform_space α} {ub : uniform_space β} {uc : uniform_space γ} (ha : ua uas) (hb : ub ubs) (hf : uniform_continuous (λ (p : α × β), f p.fst p.snd)) :
uniform_continuous (λ (p : α × β), f p.fst p.snd)

A version of uniform_continuous_Inf_dom for binary functions

def uniform_continuous₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] (f : α β γ) :
Prop

Uniform continuity for functions of two variables.

Equations
theorem uniform_continuous₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] {f : α β γ} {g : γ δ} (hg : uniform_continuous g) (hf : uniform_continuous₂ f) :
theorem uniform_continuous₂.bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {δ' : Type u_6} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] [uniform_space δ'] {f : α β γ} {ga : δ α} {gb : δ' β} (hf : uniform_continuous₂ f) (hga : uniform_continuous ga) (hgb : uniform_continuous gb) :
def uniform_space.core.sum {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :

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
theorem union_mem_uniformity_sum {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {a : set × α)} (ha : a uniformity α) {b : set × β)} (hb : b uniformity β) :
(λ (p : α × α), (sum.inl p.fst, sum.inl p.snd)) '' a (λ (p : β × β), (sum.inr p.fst, sum.inr p.snd)) '' b uniform_space.core.sum.uniformity

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

theorem uniformity_sum_of_open_aux {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set β)} (hs : is_open s) {x : α β} (xs : x s) :
{p : β) × β) | p.fst = x p.snd s} uniform_space.core.sum.uniformity
theorem open_of_uniformity_sum_aux {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set β)} (hs : (x : α β), x s {p : β) × β) | p.fst = x p.snd s} uniform_space.core.sum.uniformity) :
theorem sum.uniformity {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniformity β) = filter.map (λ (p : α × α), (sum.inl p.fst, sum.inl p.snd)) (uniformity α) filter.map (λ (p : β × β), (sum.inr p.fst, sum.inr p.snd)) (uniformity β)
theorem lebesgue_number_lemma {α : Type u} [uniform_space α] {s : set α} {ι : Sort u_1} {c : ι set α} (hs : is_compact s) (hc₁ : (i : ι), is_open (c i)) (hc₂ : s (i : ι), c i) :
(n : set × α)) (H : n uniformity α), (x : α), x s ( (i : ι), {y : α | (x, y) n} c 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 lebesgue_number_lemma_sUnion {α : Type u} [uniform_space α] {s : set α} {c : set (set α)} (hs : is_compact s) (hc₁ : (t : set α), t c is_open t) (hc₂ : s ⋃₀ c) :
(n : set × α)) (H : n uniformity α), (x : α), x s ( (t : set α) (H : t c), (y : α), (x, y) n y t)

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 lebesgue_number_of_compact_open {α : Type u_1} [uniform_space α] {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set × α)) (H : V uniformity α), is_open V (x : α), x K uniform_space.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 u_1} {β : Type u_2} [uniform_space α] {f : filter β} {u : β α} {a : α} :
filter.tendsto u f (nhds a) filter.tendsto (λ (x : β), (a, u x)) f (uniformity α)
theorem uniform.tendsto_nhds_left {α : Type u_1} {β : Type u_2} [uniform_space α] {f : filter β} {u : β α} {a : α} :
filter.tendsto u f (nhds a) filter.tendsto (λ (x : β), (u x, a)) f (uniformity α)
theorem uniform.continuous_at_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {b : β} :
continuous_at f b filter.tendsto (λ (x : β), (f b, f x)) (nhds b) (uniformity α)
theorem uniform.continuous_at_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {b : β} :
continuous_at f b filter.tendsto (λ (x : β), (f x, f b)) (nhds b) (uniformity α)
theorem uniform.continuous_at_iff_prod {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {b : β} :
continuous_at f b filter.tendsto (λ (x : β × β), (f x.fst, f x.snd)) (nhds (b, b)) (uniformity α)
theorem uniform.continuous_within_at_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {b : β} {s : set β} :
continuous_within_at f s b filter.tendsto (λ (x : β), (f b, f x)) (nhds_within b s) (uniformity α)
theorem uniform.continuous_within_at_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {b : β} {s : set β} :
continuous_within_at f s b filter.tendsto (λ (x : β), (f x, f b)) (nhds_within b s) (uniformity α)
theorem uniform.continuous_on_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {s : set β} :
continuous_on f s (b : β), b s filter.tendsto (λ (x : β), (f b, f x)) (nhds_within b s) (uniformity α)
theorem uniform.continuous_on_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} {s : set β} :
continuous_on f s (b : β), b s filter.tendsto (λ (x : β), (f x, f b)) (nhds_within b s) (uniformity α)
theorem uniform.continuous_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} :
continuous f (b : β), filter.tendsto (λ (x : β), (f b, f x)) (nhds b) (uniformity α)
theorem uniform.continuous_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β α} :
continuous f (b : β), filter.tendsto (λ (x : β), (f x, f b)) (nhds b) (uniformity α)
theorem filter.tendsto.congr_uniformity {α : Type u_1} {β : Type u_2} [uniform_space β] {f g : α β} {l : filter α} {b : β} (hf : filter.tendsto f l (nhds b)) (hg : filter.tendsto (λ (x : α), (f x, g x)) l (uniformity β)) :
theorem uniform.tendsto_congr {α : Type u_1} {β : Type u_2} [uniform_space β] {f g : α β} {l : filter α} {b : β} (hfg : filter.tendsto (λ (x : α), (f x, g x)) l (uniformity β)) :