Topology of R

InstanceMetric structure#

Instantiate the reals as a metric space.

Real.metricSpace : MetricSpace ℝ

Sources

• Mathlib documentation: Real.metricSpace
• Source of Real.metricSpace in Mathlib/Topology/MetricSpace/Basic.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Topology of R

MathlibReal.metricSpace

Uses 1 · Used by 23

Statement usesMetric space

Used byFundamental Theorem of Integral Calculus · The Non-Denumerability of the Continuum · Stirling’s Formula · Fundamental theorem of calculus, part 2 · Divergence theorem · Fubini's theorem · Banach open mapping theorem · Translation numbers define a group action up to semiconjugacy · Strong law of large numbers · Urysohn's lemma · Monotone convergence theorem (1000+ theorems) · Rademacher's theorem · Hahn decomposition theorem · Whitney embedding theorem · Dirichlet's approximation theorem · Slutsky's theorem · Continuity of integrals with respect to parameters · Cauchy-Lipschitz Theorem · Borel-Cantelli lemma (difficult direction) · Continuity (continuity and differentiability of convex functions) · Comparison of a series and an integral · Completeness of \(L^2\) · Hilbert projection theorem

TheoremCompleteness of R#

Mathlib states this as Real.instCompleteSpace.

Real.instCompleteSpace : CompleteSpace ℝ

Sources

• Mathlib documentation: Real.instCompleteSpace
• Source of Real.instCompleteSpace in Mathlib/Topology/UniformSpace/Real.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Topology of R

MathlibReal.instCompleteSpace

Uses 7 · Used by 35

Statement usesBornology · Completeness · Order

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

Used byFundamental Theorem of Integral Calculus · The Non-Denumerability of the Continuum · Minkowski’s Fundamental Theorem · Divergence of the Prime Reciprocal Series · Stirling’s Formula · First Main Theorem of Value Distribution Theory · Jensen's inequality (integral version) · Riemann-Lebesgue lemma (Analysis) · Eigenvalues from Rayleigh quotient · Existence of Hilbert basis · Fundamental theorem of calculus, part 1 · Fundamental theorem of calculus, part 2 · Approximation by convolution · Fubini's theorem · Absolutely convergent series in Banach spaces · Translation numbers define a group action up to semiconjugacy · Strong law of large numbers · Conditional expectation · Abel's theorem · Monotone convergence theorem (1000+ theorems) · Rademacher's theorem · Hahn decomposition theorem · Prokhorov's theorem · Fourier theorem · Tietze extension theorem · Whitney embedding theorem · Dirichlet's approximation theorem · Slutsky's theorem · Cos (power series expansion of elementary functions) · Sin (power series expansion of elementary functions) · Cauchy formulas · Alternating series · Comparison of a series and an integral · Geometric series · Completeness of \(L^2\)

TheoremBolzano-Weierstrass theorem (Topology of R)#

A version of Bolzano-Weierstrass: in a proper metric space (e.g. \(ℝ^n\)), every bounded sequence has a converging subsequence.

tendsto_subseq_of_bounded.{u_1} {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X}
  (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∀ (n : ℕ), x n ∈ s) :
  ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

Sources

• Mathlib documentation: tendsto_subseq_of_bounded
• Source of tendsto_subseq_of_bounded in Mathlib/Topology/MetricSpace/Sequences.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Topology of R

Mathlibtendsto_subseq_of_bounded

Uses 5

Statement usesBornology · Closure · Compactness in terms of filters · Order

Proof usesBolzano–Weierstrass theorem (1000+ theorems)

• Compact subsets of \(\R\)

TheoremConnected subsets of \(\R\)#

In a dense conditionally complete linear order, the set of preconnected sets is exactly the set of the intervals Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, (-∞, +∞), or ∅. Though one can represent ∅ as (sInf s, sInf s), we include it into the list of possible cases to improve readability.

setOfPred_isPreconnected_eq_of_ordered.{u} {α : Type u} [TopologicalSpace α]
  [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] :
  {s | IsPreconnected s} =
    Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪
          Set.range (Function.uncurry Set.Ioc) ∪
        Set.range (Function.uncurry Set.Ioo) ∪
      (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪
        {Set.univ, ∅})

Sources

• Mathlib documentation: setOfPred_isPreconnected_eq_of_ordered
• Source of setOfPred_isPreconnected_eq_of_ordered in Mathlib/Topology/Order/IntermediateValue.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Topology of R

MathlibsetOfPred_isPreconnected_eq_of_ordered

Uses 4

Statement usesOrder topology

Proof usesClosure · Continuous function · Limit of a map with respect to filters

TheoremAdditive subgroups of \(\R\)#

An additive subgroup of an archimedean linear ordered additive commutative group G with order topology either is dense in G or is a cyclic subgroup.

AddSubgroup.dense_or_isCyclic.{u_1} {G : Type u_1} [AddCommGroup G] [LinearOrder G]
  [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G]
  (H : AddSubgroup G) : Dense ↑H ∨ IsAddCyclic ↥H

Sources

• Mathlib documentation: AddSubgroup.dense_or_isCyclic
• Source of AddSubgroup.dense_or_isCyclic in Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Topology of R

MathlibAddSubgroup.dense_or_isCyclic

Uses 3

Statement usesClosure · Integer · Order topology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.