Revision #1527 → #1792 · back to history
addedMonotone convergence theorem73db57c980a7
addedIntermediate value theorem5040814bbfd8
addedMean value theorem24390521a279
modifiedReal-valued sequence09624e970ff1
| Field | From #1527 | To #1792 |
|---|
| anchors | [{"section":"Sequences","snippet":"a real-valued sequence , here indexed by the natural numbers, is a map"},{"type":"math_alttext","value":"{\\displaystyle (a_{n})=(a_{n})_{n\\in \\mathbb {N} }=(a_{1},a_{2},a_{3},\\dots ).}"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\leq a_{2}\\leq a_{3}\\leq \\cdots }"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\geq a_{2}\\geq a_{3}\\geq \\cdots }"}] | — |
modifiedConvergent and divergent sequence14a0efe0fb05
| Field | From #1527 | To #1792 |
|---|
| anchors | [{"section":"Sequences","snippet":"is said to be convergent ; otherwise it is divergent"},{"type":"math_alttext","value":"{\\displaystyle (a_{n})=(a_{n})_{n\\in \\mathbb {N} }=(a_{1},a_{2},a_{3},\\dots ).}"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\leq a_{2}\\leq a_{3}\\leq \\cdots }"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\geq a_{2}\\geq a_{3}\\geq \\cdots }"}] | — |
modifiedBounded sequence553003b1f1b5
| Field | From #1527 | To #1792 |
|---|
| anchors | [{"section":"Sequences","snippet":"is bounded if there exists"},{"type":"math_alttext","value":"{\\displaystyle (a_{n})=(a_{n})_{n\\in \\mathbb {N} }=(a_{1},a_{2},a_{3},\\dots ).}"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\leq a_{2}\\leq a_{3}\\leq \\cdots }"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\geq a_{2}\\geq a_{3}\\geq \\cdots }"}] | — |
modifiedMonotonic sequencebf9c1e5893a4
| Field | From #1527 | To #1792 |
|---|
| anchors | [{"section":"Sequences","snippet":"is monotonically increasing or decreasing if"},{"type":"math_alttext","value":"{\\displaystyle (a_{n})=(a_{n})_{n\\in \\mathbb {N} }=(a_{1},a_{2},a_{3},\\dots ).}"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\leq a_{2}\\leq a_{3}\\leq \\cdots }"},{"type":"math_alttext","value":"{\\displaystyle a_{1}\\geq a_{2}\\geq a_{3}\\geq \\cdots }"}] | — |
modifiedLimit of a function (ε-δ)73d48a59f6e3
| Field | From #1527 | To #1792 |
|---|
| anchors | [{"section":"Limits and convergence","snippet":"be a real-valued function defined on"},{"type":"math_alttext","value":"{\\displaystyle f(x)\\to L\\ \\ {\\text{as}}\\ \\ x\\to x_{0},}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{x\\to x_{0}}f(x)=L.}"}] | — |
addedUniform limit of continuous functions is continuous5b8ceaeae02b
modifiedCantor ternary set is compact068a8017db43
| Field | From #1527 | To #1792 |
|---|
| mathlib.decl | — | isCompact_cantorSet |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Instances.CantorSet |
| note | The middle-thirds Cantor ternary set as a compact subset of ℝ is not defined in Mathlib (only abstract Cantor schemes/perfect sets are). | isCompact_cantorSet proves the middle-thirds Cantor ternary set (cantorSet) is compact in ℝ. |
| status | not_formalized | formalized |
addedWeierstrass nowhere differentiable continuous function8c7175fa4eb8
addedRiemann rearrangement theoremce1e9e1a05c8
modifiedHarmonic series (divergent)d8698c02f57d
| Field | From #1527 | To #1792 |
|---|
| note | not_summable_one_div_natCast proves the harmonic series ∑ 1/n is not summable (diverges). | Real.not_summable_one_div_natCast proves the harmonic series ∑ 1/n is not summable (diverges). |
addedRadius of convergencef3d77fa262e5
addedLebesgue integralbdf44e279297
addedBolzano–Weierstrass theorem1c4744bb7de0
addedBaire category theorem54fca6a13966
addedL'Hôpital's rulee318dd215cf5
addedTaylor's theorem380618d3847a
addedDini's theorem65b376e0a999
addedArzelà–Ascoli theorem4521babf18c6
addedStone–Weierstrass theorem6d969e68a5f1
addedBanach fixed-point theorem155171f7ecc4
addedInverse function theoreme508b275ebc0
addedImplicit function theorem316e097b56b9
addedStokes' theorem99a9ab1ebb38
addedEgorov's theorem9aba369cf433
addedLusin's theorem1124ad61c6e4
addedFatou's lemmadedcbe979f41
addedMonotone convergence theorem (Lebesgue)78e309cc19d1
addedDominated convergence theorem9cd28eb2b58e
addedFubini's theorem2a9cf2a440c0
addedRadon–Nikodym theorem4e97b0c159a4
addedLebesgue differentiation theoremc5d50fb93f9a
addedHahn–Banach theorem87d45235f5c8
addedBanach–Alaoglu theorem2e71767f6560
addedRiesz representation theoremb18f07581113
addedPlancherel theoremc4a6c0c77986