Topological algebra

ClassOrder topology#

The order topology on an ordered type is the topology generated by open intervals. We register it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed. We define it as a mixin. If you want to introduce the order topology on a preorder, use Preorder.topology.

OrderTopology.{u_1} (α : Type u_1) [t : TopologicalSpace α] [Preorder α] : Prop
Sources
MathlibOrderTopology
Uses 1 · Used by 47
Statement usesTopological space
Used byFundamental Theorem of Integral Calculus · Liouville’s Theorem and the Construction of Transcendental Numbers · The Non-Denumerability of the Continuum · Divergence of the Harmonic Series · Sum of a Geometric Series · Divergence of the Prime Reciprocal Series · Stirling’s Formula · Jensen's inequality (integral version) · Local extrema · Fatou's lemma · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Monotone convergence theorem (Measures and integral calculus) · Stieltjes measure · Uniqueness of integral curves · Markov inequality · Urysohn's lemma · Intermediate value theorem · Besicovitch covering theorem · Darboux's theorem (analysis) · Monotone convergence theorem (1000+ theorems) · Rademacher's theorem · Squeeze theorem · Carathéodory's extension theorem · Hahn decomposition theorem · Vitali covering theorem · Mahler's theorem · Ostrowski's theorem · Pentagonal number theorem · Approximation by step functions · Partial derivatives commute · Grönwall lemma · Borel-Cantelli lemma (easy direction) · Continuity (Complex-valued series) · Continuity (continuity and differentiability of convex functions) · Comparison of a series and an integral · Convergence of \(p\)-series for \(p>1\) · Geometric series · Continuity of inverse functions · Continuity of monotone functions · Image of a segment · Continuity of the sum of a series of functions · Weierstrass polynomial approximation theorem · Additive subgroups of \(\R\) · Connected subsets of \(\R\) · Completeness of \(l^2\) · Completeness of \(L^2\)

TheoremIntermediate value theorem#

Intermediate Value Theorem for continuous functions on closed intervals, case f a ≤ t ≤ f b.

intermediate_value_Icc.{u, u_1} {α : Type u} [TopologicalSpace α]
  [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1}
  [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ}
  (hf : ContinuousOn f (Set.Icc a b)) : Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
Sources
Mathlibintermediate_value_Icc
Uses 4 · Used by 1
Statement usesLimit of a map with respect to filters · Order topology
Proof usesClosure · Continuous function
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem)

TheoremExtreme value theorem#

The extreme value theorem: a continuous function realizes its minimum on a compact set.

IsCompact.exists_isMinOn.{u_2, u_3} {α : Type u_2} {β : Type u_3} [LinearOrder α]
  [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s)
  (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x
Sources
MathlibIsCompact.exists_isMinOn
Uses 2 · Used by 6
Statement usesCompactness in terms of filters · Limit of a map with respect to filters
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · Rolle's theorem · Darboux's theorem (analysis) · Open mapping theorem (complex analysis) · Krein–Milman theorem · Holomorphic stability under uniform convergence

DefinitionLimit infimum and supremum#

Defines the liminf/limsup of a function taking values in a conditionally complete lattice, with respect to an arbitrary filter.

Mathlib covers this with the module Mathlib.Order.LiminfLimsup rather than a single declaration.

Its 34 documented declarations include Filter.limsSup, Filter.limsInf, Filter.limsup, Filter.liminf, Filter.blimsup, Filter.bliminf, Filter.limsup_const_bot, Filter.liminf_const_top, Filter.limsup_eq_iInf_iSup, Filter.liminf_eq_iSup_iInf, CompleteLatticeHom.apply_limsup_iterate, CompleteLatticeHom.apply_liminf_iterate, and 22 more.

Sources
MathlibFilter.limsSup · Filter.limsInf · Filter.limsup · Filter.liminf · Filter.blimsup · Filter.bliminf · Filter.limsup_const_bot · Filter.liminf_const_top · Filter.limsup_eq_iInf_iSup · Filter.liminf_eq_iSup_iInf · CompleteLatticeHom.apply_limsup_iterate · CompleteLatticeHom.apply_liminf_iterate

ClassTopological group#

A topological group is a group in which the multiplication and inversion operations are continuous.

When you declare an instance that does not already have a UniformSpace instance, you should also provide an instance of UniformSpace and IsUniformGroup using IsTopologicalGroup.rightUniformSpace and isUniformGroup_of_commGroup.

IsTopologicalGroup.{u_4} (G : Type u_4) [TopologicalSpace G] [Group G] : Prop
Sources
MathlibIsTopologicalGroup
Uses 3 · Used by 2
Statement usesContinuous function · Group · Integer
Used byHaar measure on a locally compact Hausdorff group · Steinhaus theorem

InstanceCompletion of an abelian topological group#

Mathlib states this as UniformSpace.Completion.instAddCommGroup.

UniformSpace.Completion.instAddCommGroup.{u_3} {α : Type u_3} [UniformSpace α] [AddCommGroup α]
  [IsUniformAddGroup α] : AddCommGroup (UniformSpace.Completion α)
Sources
MathlibUniformSpace.Completion.instAddCommGroup
Uses 2 · Used by 3
Statement usesCompletion · Integer
Used byLiouville theorem · Maximum modulus principle · Completion of a topological ring

DefinitionInfinite sum#

HasSum f a L means that the (potentially infinite) sum of the f b for b : β converges to a along the SummationFilter L.

By default L is the unconditional one, corresponding to the limit of all finite sets towards the entire type. So we take the sum over bigger and bigger finite sets. This sum operation is invariant under permuting the terms (while sums for more general summation filters usually are not). This is based on Mario Carneiro's infinite sum df-tsms in Metamath.

In particular, the function ℕ → ℝ sending n to (-1) ^ n / (n + 1) does not have a sum for this definition, although it is summable for the conditional summation filter that takes limits of sums over n ∈ {0, ..., X} as X → ∞. However, a series which is absolutely convergent with respect to the conditional summation filter is in fact unconditionally summable.

For the definition and many statements, α does not need to be a topological additive monoid, only an additive monoid with a topology (i.e. the addition is not assumed to be continuous). We only add this assumption later, for the lemmas where it is relevant.

HasSum.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (a : α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop
Sources
MathlibHasSum
Uses 4 · Used by 39
Statement usesFinite set · Limit of a map with respect to filters · Natural number · Topological space
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · The Non-Denumerability of the Continuum · Divergence of the Harmonic Series · Sum of a Geometric Series · Divergence of the Prime Reciprocal Series · Stirling’s Formula · Analytic function · Positive measure · Absolutely convergent series in Banach spaces · Liouville's theorem on existence of transcendental numbers · Smooth immersion · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · (smooth) vector bundle · Almost sure convergence · Discrete law · Gromov-Hausdorff space · Abel's theorem · Carathéodory's theorem (measure theory) · Hahn decomposition theorem · Metrization theorems · Glaisher's theorem · Mahler's theorem · Pentagonal number theorem · Matrix exponential · Borel-Cantelli lemma (easy direction) · Continuity (Complex-valued series) · Differentiability with respect to the complex variable · Cos (power series expansion of elementary functions) · Log · Sin (power series expansion of elementary functions) · Convergence of \(p\)-series for \(p>1\) · Geometric series · Continuity of the sum of a series of functions · Differentiability of the sum of a series of functions · Taylor's theorem with Lagrange form for remainder · Completeness of \(l^2\) · Hilbert bases · Inner product space \(l^2\)

ClassTopological ring#

A topological ring is a ring R where addition, multiplication and negation are continuous.

If R is a (unital) ring, then continuity of negation can be derived from continuity of multiplication as it is multiplication with -1. (See IsTopologicalSemiring.continuousNeg_of_mul and IsTopologicalSemiring.toIsTopologicalRing)

IsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : Prop
Sources
MathlibIsTopologicalRing
Uses 2 · Used by 56
Statement usesContinuous function · Integer
Used byFundamental Theorem of Integral Calculus · Liouville’s Theorem and the Construction of Transcendental Numbers · The Non-Denumerability of the Continuum · Fourier Series · L’Hopital’s Rule · Sum of a Geometric Series · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Buffon Needle Problem · Leibniz formula (Analysis) · Local extrema · Mean value theorem (Differentiability) · Eigenvalues from Rayleigh quotient · Fréchet-Riesz representation of the dual of a Hilbert space · Fundamental theorem of calculus, part 2 · Finite-dimensional normed spaces over complete normed fields are complete · Hahn-Banach theorem · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Isometric inclusion in double dual · Translation numbers define a group action up to semiconjugacy · Sphere · Closed interval · Riemannian/bundle metric · Smooth bundle metric · Strong law of large numbers · Stone-Weierstrass theorem · Urysohn's lemma · Completion of a topological ring · Abel's theorem · Monotone convergence theorem (1000+ theorems) · Fernique's theorem · Vitali covering theorem · Banach–Alaoglu theorem · Whitney embedding theorem · Glaisher's theorem · Ostrowski's theorem · Pentagonal number theorem · Poisson limit theorem · Slutsky's theorem · Matrix exponential · Inverse function theorem (Differential calculus) · Partial derivatives commute · Grönwall lemma · Continuity (Complex-valued series) · Holomorphic stability under uniform convergence · Continuity (continuity and differentiability of convex functions) · Derivative of the inverse of a function (Single Variable Real Analysis) · Leibniz formula (Single Variable Real Analysis) · Change of variable · Alternating series · Geometric series · Weierstrass polynomial approximation theorem · Weierstrass trigonometric approximation theorem · Taylor's theorem with Lagrange form for remainder · Completeness of \(l^2\) · Completeness of \(L^2\) · Hilbert projection theorem

InstanceCompletion of a topological ring#

Mathlib states this as UniformSpace.Completion.ring.

UniformSpace.Completion.ring.{u_1} {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α]
  [IsUniformAddGroup α] : Ring (UniformSpace.Completion α)
Sources
MathlibUniformSpace.Completion.ring
Uses 3
Statement usesCompletion of an abelian topological group · Ring · Topological ring

ClassTopological module#

Class ContinuousSMul M X says that the scalar multiplication (•) : M → X → X is continuous in both arguments. We use the same class for all kinds of multiplicative actions, including (semi)modules and algebras.

ContinuousSMul.{u_1, u_2} (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace M]
  [TopologicalSpace X] : Prop
Sources
MathlibContinuousSMul
Uses 1 · Used by 41
Statement usesContinuous function
Used byFundamental Theorem of Integral Calculus · Derivative of a composition of functions (Analysis) · Derivative of the inverse of a function (Analysis) · Local extrema · Eigenvalues from Rayleigh quotient · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Fubini's theorem · Banach-Steinhaus theorem · Equivalence of norms in finite dimension · Finite-dimensional normed spaces over complete normed fields are complete · Isometric inclusion in double dual · Translation numbers define a group action up to semiconjugacy · Integral curves · Local existence of integral curves · Uniqueness of integral curves · Smooth bundle metric · Covariant derivatives · (smooth) Hom bundle · Strong law of large numbers · Conditional expectation · Urysohn's lemma · Darboux's theorem (analysis) · Krein–Milman theorem · Mahler's theorem · Poisson limit theorem · Stability by multiplication by a slowly growing smooth function · \(L^p\) functions · Riemann-Lebesgue lemma (Measures and integral calculus) · Continuity of integrals with respect to parameters · Chain rule · Inverse function theorem (Differential calculus) · Cauchy-Lipschitz Theorem · Grönwall lemma · Continuity (continuity and differentiability of convex functions) · Derivative at a point · Derivative of the inverse of a function (Single Variable Real Analysis) · Differentiability of the sum of a series of functions · Weierstrass polynomial approximation theorem · Hilbert projection theorem · Riesz' lemma (unit-ball characterization of finite dimension)

StructureContinuous linear map#

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

ContinuousLinearMap.{u_1, u_2, u_3, u_4} {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S]
  (σ : R →+* S) (M : Type u_3) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type u_4)
  [TopologicalSpace M₂] [AddCommMonoid M₂] [_root_.Module R M] [_root_.Module S M₂] :
  Type (max u_3 u_4)
Sources
MathlibContinuousLinearMap
Uses 2 · Used by 29
Statement usesContinuous function · Linear map
Used byDifferentiable function between normed vector spaces · Implicit function theorem · Inverse function theorem (Differentiability) · Eigenvalues from Rayleigh quotient · Orthogonal projection · Banach open mapping theorem · Banach-Steinhaus theorem · Dual of a normed space · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Norm of a continuous linear map · Integral curves · Pullback of vector fields · Tangent map · Riemannian/bundle metric · Covariant derivatives · Topological vector bundle · Abel's theorem · Rademacher's theorem · Inscribed angle theorem · Fourier transforms · Inverse Fourier transform · Differentials (linear tangent functions) · Inverse function theorem (Differential calculus) · Cauchy-Lipschitz Theorem · Grönwall lemma · Holomorphic functions · Derivative at a point · Derivative of the inverse of a function (Single Variable Real Analysis) · Riemann sums

DefinitionHaar measure on a locally compact Hausdorff group#

The Haar measure on the locally compact group G, scaled so that haarMeasure K₀ K₀ = 1.

MeasureTheory.Measure.haarMeasure.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G]
  (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure G
Sources
MathlibMeasureTheory.Measure.haarMeasure
Uses 9
Statement usesAssociative algebra over a commutative ring · Borel sigma-algebra · Bornology · Carathéodory's theorem (measure theory) · Closure · Compactness in terms of filters · Order · Positive measure · Topological group

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.