Filter to Topological vector bundle

StructureFilter#

A filter F on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. We do not forbid this collection to be all sets of α.

Filter.{u_1} (α : Type u_1) : Type u_1
Sources
MathlibFilter
Uses 1 · Used by 10
Statement usesSet
Used byBornology · Local convexity · Omega-limit sets · Hyper-real number · Cluster point · Extension by continuity · Limit of a map with respect to filters · Stone-Cech compactification · Going-up and going-down theorems · Łoś' theorem

DefinitionLimit of a map with respect to filters#

Filter.Tendsto is the generic "limit of a function" predicate. Tendsto f l₁ l₂ asserts that for every l₂ neighborhood a, the f-preimage of a is an l₁ neighborhood.

Filter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α)
  (l₂ : Filter β) : Prop
Sources
MathlibFilter.Tendsto
Uses 1 · Used by 14
Statement usesFilter
Used byDirichlet class number formula · 0-manifolds are discrete spaces · Sequential space · Topological fiber bundle · Extreme value theorem · Infinite sum · Intermediate value theorem · Uniform space · Squeeze theorem · Tychonoff's theorem · Diffeomorphisms · Image of a segment · Pointwise convergence · Connected subsets of \(\R\)

ClassTopological space#

A topology on X.

TopologicalSpace.{u} (X : Type u) : Type u
Sources
MathlibTopologicalSpace
Uses 1 · Used by 21
Statement usesSet
Used byBorel sigma-algebra · Local convexity · Presheafed space · Sheafed space · Zariski topology · 0-manifolds are discrete spaces · Closed map · Closure · Cluster point · Connectedness · Continuous function · Hausdorff space · Induced topology · Open map · Sequential space · The category of topological spaces · Infinite sum · Order topology · Uniform space · Pointwise convergence · Connected components

StructureContinuous function#

A function between topological spaces is continuous if the preimage of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.

Continuous.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
  Prop
Sources
MathlibContinuous
Uses 1 · Used by 46
Statement usesTopological space
Used byDivergence of the Harmonic Series · Minkowski’s Fundamental Theorem · Divergence of the Prime Reciprocal Series · \(L^p\) space · Uniform integrability · Vector-valued integrable function (Bochner integral) · Completeness of spaces of bounded continuous functions · Hindman's theorem (Ramsey theory) · Presheafed space · Sheafed space · Hensel's lemma (for \(\mathbb{Z}_p\)) · Boundary of a manifold · Interior of a manifold · Lie algebra of a Lie group · Tangent bundle · Markov inequality · Compact open topology · Urysohn's lemma · Arzela-Ascoli theorem · Continuous linear map · Intermediate value theorem · Topological group · Topological module · Topological ring · Heine-Cantor theorem · Dini's theorem · Bounded convergence theorem · Carathéodory's extension theorem · Vitali convergence theorem · Closed graph theorem · Hellinger–Toeplitz theorem · Hindman's theorem (1000+ theorems) · Tietze extension theorem · Dirichlet's approximation theorem · Continuous mapping theorem · Slutsky's theorem · Approximation by step functions · Radius of convergence · Convergence of \(p\)-series for \(p>1\) · Continuity of monotone functions · Continuity of the limit of a sequence of functions · Continuity of the sum of a series of functions · Connected subsets of \(\R\) · Normed space of bounded continuous functions · Homeomorphisms · Path connectedness

StructureThe category of topological spaces#

The category of topological spaces.

TopCat.{u} : Type (u + 1)
Sources
MathlibTopCat
Uses 1 · Used by 1
Statement usesTopological space
Used byLocally ringed space

DefinitionInduced topology#

Given f : X → Y and a topology on Y, the induced topology on X is the collection of sets that are preimages of some open set in Y. This is the coarsest topology that makes f continuous.

TopologicalSpace.induced.{u_1, u_2} {X : Type u_1} {Y : Type u_2} (f : X → Y)
  (t : TopologicalSpace Y) : TopologicalSpace X
Sources
MathlibTopologicalSpace.induced
Uses 1 · Used by 13
Statement usesTopological space
Used byDerivative of the inverse of a function (Analysis) · Finite-dimensional normed spaces over complete normed fields are complete · Weak-* topology for dualities · Scheme · Disjoint union of manifolds · Smooth embedding · General linear group as a Lie group · Extension by continuity · Topological fiber bundle · Metrization theorems · Tietze extension theorem · Whitney embedding theorem · Pointwise convergence

DefinitionOpen map#

A map f : X → Y is said to be an open map, if the image of any open U : Set X is open in Y.

IsOpenMap.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
  Prop
Sources
MathlibIsOpenMap
Uses 1 · Used by 3
Statement usesTopological space
Used byBanach open mapping theorem · Scheme · General linear group as a Lie group

DefinitionClosed map#

A map f : X → Y is said to be a closed map, if the image of any closed U : Set X is closed in Y.

IsClosedMap.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
  Prop
Sources
MathlibIsClosedMap
Uses 1 · Used by 1
Statement usesTopological space
Used byTietze extension theorem

DefinitionClosure#

The closure of s is the smallest closed set containing s.

closure.{u} {X : Type u} [TopologicalSpace X] (s : Set X) : Set X
Sources
Mathlibclosure
Uses 1 · Used by 46
Statement usesTopological space
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · L’Hopital’s Rule · Sum of a Geometric Series · Phragmen-Lindelöf principle · Test functions · Existence of Hilbert basis · Fatou's lemma · Finite-dimensional normed spaces over complete normed fields are complete · Behrend's construction · Translation numbers define a group action up to semiconjugacy · Omega-limit sets · Boundary of a manifold · Jacobi/Leibniz identity · Uniqueness of integral curves · Extension by continuity · Stone-Weierstrass theorem · Urysohn's lemma · Arzela-Ascoli theorem · Baire theorem · Haar measure on a locally compact Hausdorff group · Intermediate value theorem · Besicovitch covering theorem · Bolzano–Weierstrass theorem (1000+ theorems) · Prokhorov's theorem · Steinhaus theorem · Vitali convergence theorem · Vitali covering theorem · Hadamard three-lines theorem · Banach–Alaoglu theorem · Krein–Milman theorem · Whitney embedding theorem · Dirichlet's approximation theorem · Glaisher's theorem · Mahler's theorem · Pentagonal number theorem · Approximation by step functions · Grönwall lemma · Differentiability of the sum of a series of functions · Weierstrass polynomial approximation theorem · Weierstrass trigonometric approximation theorem · Taylor's theorem with Lagrange form for remainder · Additive subgroups of \(\R\) · Bolzano-Weierstrass theorem (Topology of R) · Connected subsets of \(\R\) · Completeness of \(L^2\) · Example, the Hilbert basis of trigonometric polynomials

DefinitionCluster point#

A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥. Also known as an accumulation point or a limit point, but beware that terminology varies. This is not the same as asking 𝓝[≠] x ⊓ F ≠ ⊥, which is called AccPt in Mathlib. See mem_closure_iff_clusterPt in particular.

ClusterPt.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) : Prop
Sources
MathlibClusterPt
Uses 2 · Used by 9
Statement usesFilter · Topological space
Used byLocal extrema · Fatou's lemma · Jacobi/Leibniz identity · Compactness in terms of filters · Monotone convergence theorem (1000+ theorems) · Vitali convergence theorem · Limit point · Taylor's theorem with Lagrange form for remainder · Completeness of \(L^2\)

ClassHausdorff space#

A T₂ space, also known as a Hausdorff space, is one in which for every x ≠ y there exists disjoint open sets around x and y. This is the most widely used of the separation axioms.

T2Space.{u} (X : Type u) [TopologicalSpace X] : Prop
Sources
MathlibT2Space
Uses 1 · Used by 45
Statement usesTopological space
Used byThe Area of a Circle · The Non-Denumerability of the Continuum · Stirling’s Formula · Principle of isolated zeros · Leibniz formula (Analysis) · Existence of Hilbert basis · Divergence theorem · Fubini's theorem · Regularization by convolution · Banach open mapping theorem · Equivalence of norms in finite dimension · Finite-dimensional normed spaces over complete normed fields are complete · Hindman's theorem (Ramsey theory) · Translation numbers define a group action up to semiconjugacy · Uniform time existence · Uniqueness of integral curves · Strong law of large numbers · Stone-Cech compactification · Urysohn's lemma · Arzela-Ascoli theorem · Contraction mapping theorem · Heine-Borel theorem (proper metric space version) · Abel's theorem · Monotone convergence theorem (1000+ theorems) · Carathéodory's extension theorem · Hahn decomposition theorem · Prokhorov's theorem · Hellinger–Toeplitz theorem · Hindman's theorem (1000+ theorems) · Krein–Milman theorem · Whitney embedding theorem · Glaisher's theorem · Mahler's theorem · Pentagonal number theorem · Stability by multiplication by a slowly growing smooth function · Riemann-Lebesgue lemma (Measures and integral calculus) · Chain rule · Partial derivatives commute · Comparison of a series and an integral · Geometric series · Image of a segment · Continuity of the sum of a series of functions · Completeness of \(L^2\) · Hilbert projection theorem · Riesz' lemma (unit-ball characterization of finite dimension)

ClassSequential space#

A topological space is said to be a sequential space if any sequentially closed set in this space is closed. This condition is weaker than being a Fréchet-Urysohn space.

SequentialSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : Prop
Sources
MathlibSequentialSpace
Uses 3 · Used by 2
Statement usesLimit of a map with respect to filters · Natural number · Topological space
Used byMahler's theorem · Differentiability of the sum of a series of functions

DefinitionExtension by continuity#

If i : α → β is a dense inducing, then any function f : α → γ "extends" to a function g = IsDenseInducing.extend di f : β → γ. If γ is Hausdorff and f has a continuous extension, then g is the unique such extension. In general, g might not be continuous or even extend f.

IsDenseInducing.extend.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Type u_3}
  [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ]
  (di : IsDenseInducing i) (f : α → γ) (b : β) : γ
Sources
MathlibIsDenseInducing.extend
Uses 3 · Used by 5
Statement usesClosure · Filter · Induced topology
Used byAdjoint operator · Bochner integral · Conditional expectation · \(L^p\) functions · Fourier transform on \(\mathrm{L}^2(\R^d)\)

DefinitionCompactness in terms of filters#

A set s is compact if for every nontrivial filter f that contains s, there exists a ∈ s such that every set of f meets every neighborhood of a.

IsCompact.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop
Sources
MathlibIsCompact
Uses 1 · Used by 44
Statement usesCluster point
Used byFundamental Theorem of Integral Calculus · Minkowski’s Fundamental Theorem · Buffon Needle Problem · First Main Theorem of Value Distribution Theory · Test functions · Riemann-Lebesgue lemma (Analysis) · Fundamental theorem of calculus, part 2 · Stieltjes measure · Approximation by convolution · Change of variables formula · Regularization by convolution · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Hindman's theorem (Ramsey theory) · Sphere · Strong law of large numbers · Compact open topology · Compactness in terms of open covers (Borel-Lebesgue) · Arzela-Ascoli theorem · Gromov-Hausdorff space · Heine-Borel theorem (proper metric space version) · Sequential compactness is equivalent to compactness (Bolzano-Weierstrass) · Extreme value theorem · Haar measure on a locally compact Hausdorff group · Heine-Cantor theorem · Bolzano–Weierstrass theorem (1000+ theorems) · Cantor's intersection theorem · Rademacher's theorem · Prokhorov's theorem · Steinhaus theorem · Banach–Alaoglu theorem · Hindman's theorem (1000+ theorems) · Krein–Milman theorem · Tychonoff's theorem · Whitney embedding theorem · Dirichlet's approximation theorem · Decomposition of an orthogonal transformation as a product of reflections · Orthonormal bases · Gram-Schmidt orthogonalisation · Riemann-Lebesgue lemma (Measures and integral calculus) · Differentiability of integrals with respect to parameters · Comparison of a series and an integral · Image of a segment · Bolzano-Weierstrass theorem (Topology of R) · Riesz' lemma (unit-ball characterization of finite dimension)

TheoremCompactness in terms of open covers (Borel-Lebesgue)#

A set s is compact if and only if for every open cover of s, there exists a finite subcover.

isCompact_iff_finite_subcover.{u} {X : Type u} [TopologicalSpace X] {s : Set X} :
  IsCompact s ↔
    ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
Sources
MathlibisCompact_iff_finite_subcover
Uses 2
Statement usesCompactness in terms of filters · Finite set

ClassConnectedness#

A connected space is a nonempty one where there is no non-trivial open partition.

ConnectedSpace.{u} (α : Type u) [TopologicalSpace α] : Prop
Sources
MathlibConnectedSpace
Uses 1 · Used by 3
Statement usesTopological space
Used byGelfand–Mazur theorem · Dirichlet's approximation theorem · Differentiability of the sum of a series of functions

InstanceCompact open topology#

The compact-open topology on the space of continuous maps C(X, Y).

ContinuousMap.compactOpen.{u_2, u_3} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X]
  [TopologicalSpace Y] : TopologicalSpace C(X, Y)
Sources
MathlibContinuousMap.compactOpen
Uses 2 · Used by 6
Statement usesCompactness in terms of filters · Continuous function
Used byFourier Series · Stone-Weierstrass theorem · Mahler's theorem · Weierstrass polynomial approximation theorem · Weierstrass trigonometric approximation theorem · Example, the Hilbert basis of trigonometric polynomials

DefinitionStone-Cech compactification#

The Stone-Čech compactification of a topological space.

StoneCech.{u} (α : Type u) [TopologicalSpace α] : Type u
Sources
MathlibStoneCech
Uses 2
Statement usesFilter · Hausdorff space

ClassTopological fiber bundle#

A (topological) fiber bundle with fiber F over a base B is a space projecting on B for which the fibers are all homeomorphic to F, such that the local situation around each point is a direct product.

FiberBundle.{u_2, u_3, u_5} {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F]
  (E : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] :
  Type (max (max u_2 u_3) u_5)
Sources
MathlibFiberBundle
Uses 2 · Used by 6
Statement usesInduced topology · Limit of a map with respect to filters
Used byJacobi/Leibniz identity · Local existence of integral curves · Uniform time existence · Uniqueness of integral curves · Covariant derivatives · Topological vector bundle

ClassTopological vector bundle#

The space Bundle.TotalSpace F E (for E : B → Type* such that each E x is a topological vector space) has a topological vector space structure with fiber F (denoted with VectorBundle R F E) if around every point there is a fiber bundle trivialization which is linear in the fibers.

VectorBundle.{u_1, u_2, u_3, u_4} (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4)
  [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → _root_.Module R (E x)]
  [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B]
  [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] :
  Prop
Sources
MathlibVectorBundle
Uses 3 · Used by 2
Statement usesContinuous linear map · Normed vector space over a normed field · Topological fiber bundle
Used bySmooth bundle metric · (smooth) vector bundle

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.