Topology and Metric Spaces

TheoremTopology of a metric space#

Mathlib states this as Metric.isOpen_iff.

Metric.isOpen_iff.{u} {α : Type u} [PseudoMetricSpace α] {s : Set α} :
  IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s

Sources

• Mathlib documentation: Metric.isOpen_iff
• Source of Metric.isOpen_iff in Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibMetric.isOpen_iff

Uses 3 · Used by 14

Statement usesBall

Proof usesField \(\R\) of real numbers · Ordered ring

Used byPrinciple of analytic continuation · Divergence theorem · Regularization by convolution · Banach open mapping theorem · General linear group as a Lie group · Besicovitch covering theorem · Rademacher's theorem · Vitali covering theorem · Fourier theorem · Metrization theorems · Partial derivatives commute · Continuity (continuity and differentiability of convex functions) · Differentiability of the sum of a series of functions · Riesz' lemma (unit-ball characterization of finite dimension)

• Induced topology

InstanceFinite product of metric spaces#

A finite product of metric spaces is a metric space, with the sup distance.

metricSpacePi.{v, u_2} {β : Type v} {X : β → Type u_2} [Fintype β] [(b : β) → MetricSpace (X b)] :
  MetricSpace ((b : β) → X b)

Sources

• Mathlib documentation: metricSpacePi
• Source of metricSpacePi in Mathlib/Topology/MetricSpace/Basic.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibmetricSpacePi

Uses 2

Statement usesFinite set · Metric space

TheoremLimits of sequences#

Mathlib states this as Metric.tendsto_atTop.

Metric.tendsto_atTop.{u, v} {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β]
  [SemilatticeSup β] {u : β → α} {a : α} :
  Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε

Sources

• Mathlib documentation: Metric.tendsto_atTop
• Source of Metric.tendsto_atTop in Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibMetric.tendsto_atTop

Uses 5 · Used by 4

Statement usesBornology · Order

Proof usesBall · Field \(\R\) of real numbers · Ordered ring

Used byCompleteness of spaces of bounded continuous functions · Abel's theorem · Lévy continuity theorem · Hilbert projection theorem

• Cluster points
• Continuous functions

StructureHomeomorphisms#

Homeomorphism between X and Y, also called topological isomorphism

Homeomorph.{u_4, u_5} (X : Type u_4) (Y : Type u_5) [TopologicalSpace X] [TopologicalSpace Y] :
  Type (max u_4 u_5)

Sources

• Mathlib documentation: Homeomorph
• Source of Homeomorph in Mathlib/Topology/Homeomorph/Defs.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibHomeomorph

Uses 1 · Used by 14

Statement usesContinuous function

Used byFourier Series · Lax-Milgram theorem · Regularization by convolution · Smooth immersion · Smooth or analytic manifold (with boundary and corners) · (smooth) trivial vector bundle · Rademacher's theorem · Decomposition of an orthogonal transformation as a product of reflections · Riemann-Lebesgue lemma (Measures and integral calculus) · Diffeomorphisms · Cauchy formulas · Continuity of inverse functions · Weierstrass polynomial approximation theorem · Example, the Hilbert basis of trigonometric polynomials

• Compactness in terms of open covers (Borel-Lebesgue)
• Sequential compactness is equivalent to compactness (Bolzano-Weierstrass)
• Connectedness

DefinitionConnected components#

The connected component of a point is the maximal connected set that contains this point.

connectedComponent.{u} {α : Type u} [TopologicalSpace α] (x : α) : Set α

Sources

• Mathlib documentation: connectedComponent
• Source of connectedComponent in Mathlib/Topology/Connected/Basic.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibconnectedComponent

Uses 1

Statement usesTopological space

DefinitionPath connectedness#

A set F is path connected if it contains a point that can be joined to all other in F.

IsPathConnected.{u_1} {X : Type u_1} [TopologicalSpace X] (F : Set X) : Prop

Sources

• Mathlib documentation: IsPathConnected
• Source of IsPathConnected in Mathlib/Topology/Connected/PathConnected.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibIsPathConnected

Uses 3

Statement usesBornology · Continuous function · Order

• Lipschitz functions
• Uniformly continuous functions
• Heine-Cantor theorem

TheoremComplete metric spaces#

A pseudo-metric space is complete iff every Cauchy sequence converges.

Metric.complete_of_cauchySeq_tendsto.{u} {α : Type u} [PseudoMetricSpace α] :
  (∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α

Sources

• Mathlib documentation: Metric.complete_of_cauchySeq_tendsto
• Source of Metric.complete_of_cauchySeq_tendsto in Mathlib/Topology/MetricSpace/Cauchy.lean
• Mathlib undergraduate list: Topology › Topology and Metric Spaces

MathlibMetric.complete_of_cauchySeq_tendsto

Uses 3 · Used by 3

Statement usesBornology · Completeness · Order

Used byCompleteness of spaces of bounded continuous functions · Completeness of R · Completeness of \(l^2\)

• Contraction mapping theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.