Uniform notions

ClassUniform space#

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.

UniformSpace.{u} (α : Type u) : Type u
Sources
MathlibUniformSpace
Uses 2 · Used by 6
Statement usesLimit of a map with respect to filters · Topological space
Used bySequential compactness is equivalent to compactness (Bolzano-Weierstrass) · Cauchy filter · Heine-Cantor theorem · Uniform convergence · Metrization theorems · Continuity of the limit of a sequence of functions

TheoremUniformly continuous function#

Mathlib states this as Metric.uniformContinuous_iff.

Metric.uniformContinuous_iff.{u, v} {α : Type u} {β : Type v} [PseudoMetricSpace α]
  [PseudoMetricSpace β] {f : α → β} :
  UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε
Sources
MathlibMetric.uniformContinuous_iff
Uses 4 · Used by 10
Statement usesBornology · Order
Proof usesField \(\R\) of real numbers · Ordered ring
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · The Non-Denumerability of the Continuum · Divergence of the Prime Reciprocal Series · Riemann-Lebesgue lemma (Analysis) · Change of variables formula · Completeness of spaces of bounded continuous functions · Hahn decomposition theorem · Mahler's theorem · Alternating series · Continuity of the sum of a series of functions

DefinitionUniform convergence#

A sequence of functions Fₙ converges uniformly to a limiting function f with respect to a filter p if, for any entourage of the diagonal u, one has p-eventually (f x, Fₙ x) ∈ u for all x.

TendstoUniformly.{u_1, u_2, u_4} {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β]
  (F : ι → α → β) (f : α → β) (p : Filter ι) : Prop
Sources
MathlibTendstoUniformly
Uses 1 · Used by 2
Statement usesUniform space
Used byCompleteness of spaces of bounded continuous functions · Differentiability of the limit of a sequence of functions

DefinitionCauchy filter#

A filter f is Cauchy if for every entourage r, there exists an s ∈ f such that s × s ⊆ r. This is a generalization of Cauchy sequences, because if a : ℕ → α then the filter of sets containing cofinitely many of the a n is Cauchy iff a is a Cauchy sequence.

Cauchy.{u} {α : Type u} [uniformSpace : UniformSpace α] (f : Filter α) : Prop
Sources
MathlibCauchy
Uses 1 · Used by 3
Statement usesUniform space
Used byCauchy sequence · Completeness · Completion

DefinitionCauchy sequence#

Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that is general enough to cover both ℕ and ℝ, which are the main motivating examples.

CauchySeq.{u, v} {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β]
  (u : β → α) : Prop
Sources
MathlibCauchySeq
Uses 1 · Used by 4
Statement usesCauchy filter
Used byHensel's lemma (for \(\mathbb{Z}_p\)) · \(p\)-adic number · Real number · Sequential compactness is equivalent to compactness (Bolzano-Weierstrass)

ClassCompleteness#

A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.

CompleteSpace.{u} (α : Type u) [UniformSpace α] : Prop
Sources
MathlibCompleteSpace
Uses 1 · Used by 57
Statement usesCauchy filter
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · L’Hopital’s Rule · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Removable singularity · Implicit function theorem · Inverse function theorem (Differentiability) · Mean value theorem (Differentiability) · Inner product space, over \(R\) or \(C\) · Bochner integral · Absolutely convergent series in Banach spaces · Banach open mapping theorem · Banach-Steinhaus theorem · Completeness of spaces of bounded continuous functions · Equivalence of norms in finite dimension · Finite-dimensional normed spaces over complete normed fields are complete · Hahn-Banach theorem · Isometric inclusion in double dual · Hensel's lemma (for \(\mathbb{Z}_p\)) · Boundary of a manifold · Integral curves · Interior of a manifold · Lie algebra of a Lie group · Pullback of vector fields · Smooth immersion · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · Tangent bundle · Covariant derivatives · (smooth) vector bundle · Kolmogorov's \(0\)-\(1\) law · Baire theorem · Contraction mapping theorem · Closed graph theorem · Gelfand–Mazur theorem · Akra–Bazzi theorem · Hahn embedding theorem · Mahler's theorem · Niven's theorem · Pentagonal number theorem · Poisson limit theorem · Norm · Stability by derivation · Inverse function theorem (Differential calculus) · Partial derivatives commute · Cauchy-Lipschitz Theorem · Grönwall lemma · Differentiability with respect to the complex variable · Holomorphic stability under uniform convergence · Continuity of the sum of a series of functions · Differentiability of the limit of a sequence of functions · Differentiability of the sum of a series of functions · Weierstrass trigonometric approximation theorem · Completeness of R · Completeness of \(l^2\) · Completeness of \(L^2\) · Riesz' lemma (unit-ball characterization of finite dimension) · Complete metric spaces

DefinitionCompletion#

Hausdorff completion of α

UniformSpace.Completion.{u_1} (α : Type u_1) [UniformSpace α] : Type u_1
Sources
MathlibUniformSpace.Completion
Uses 1 · Used by 2
Statement usesCauchy filter
Used by\(p\)-adic number · Completion of an abelian topological group

TheoremHeine-Cantor theorem#

Heine-Cantor: a continuous function on a compact uniform space is uniformly continuous.

CompactSpace.uniformContinuous_of_continuous.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [UniformSpace α] [UniformSpace β] [CompactSpace α] {f : α → β} (h : Continuous f) :
  UniformContinuous f
Sources
MathlibCompactSpace.uniformContinuous_of_continuous
Uses 3 · Used by 3
Statement usesCompactness in terms of filters · Continuous function · Uniform space
Used byDivergence theorem · Mahler's theorem · Weierstrass polynomial approximation theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.