Revision #1362 → #2105 · back to history
modifiedUnbounded, bounded, bounded above/below sequencesa28cd5195ce3
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Order.Bounds.Basic | Mathlib.Order.Bounds.Defs |
modifiedEuclidean distance in n-dimensional real vectorsd04a04bbd2e2
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Analysis.InnerProductSpace.EuclideanDist | Mathlib.Analysis.InnerProductSpace.PiL2 |
addedOne-sided (left/right) limit70b761951cac
modifiedLimit via standard part in nonstandard analysis48aa8c795216
| Field | From #1362 | To #2105 |
|---|
| mathlib.decl | Hyperreal.stdPart | Hyperreal.st |
| note | The standard part on `ℝ*` (and its connection to ordinary limits) is developed in `Mathlib.Analysis.Real.Hyperreal`. | The standard part on `ℝ*` is `Hyperreal.st : ℝ* → ℝ` (defined in `Mathlib.Analysis.Real.Hyperreal`). |
modifiedStandard part of ultrapower equals limit of Cauchy sequence65c5a95d7cde
| Field | From #1362 | To #2105 |
|---|
| note | `stdPart_of_tendsto` proves the standard part of a hyperreal equals the limit when one exists. | `Hyperreal.stdPart_of_tendsto` proves the standard part of a hyperreal equals the limit when one exists. |
modifiedLimit set of a sequence5c4b05cd96ab
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Topology.ClusterPt | Mathlib.Topology.Defs.Filter |
modifiedPower series and radius of convergencee1bb2c543db4
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Analysis.Analytic.Basic | Mathlib.Analysis.Analytic.ConvergenceRadius |
modifiedContinuous functions preserve limitse0823a99dede
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Topology.ContinuousOn | Mathlib.Topology.Continuous |
modifiedClosed set contains all its limit points24c97731fb07
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Topology.Order.OrderClosed | Mathlib.Topology.Neighborhoods |
modifiedSum of limits equals limit of sum23db94cd063b
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Monoid | Mathlib.Topology.Algebra.Monoid.Defs |
modifiedProduct of limits equals limit of product96dc6158194b
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Monoid | Mathlib.Topology.Algebra.Monoid.Defs |
modifiedInverse of limit equals limit of inverse22d686c9a12a
| Field | From #1362 | To #2105 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Group.Basic | Mathlib.Topology.Algebra.Group.Defs |
modifiedConvergent sequences of reals are Cauchya9a0dd1ef10a
| Field | From #1362 | To #2105 |
|---|
| note | A convergent sequence is Cauchy: lemma at `Mathlib/Topology/UniformSpace/Cauchy.lean:202` builds a `CauchySeq` from a `Tendsto … atTop (𝓝 x)`. | `Filter.Tendsto.cauchySeq` builds a `CauchySeq` from a sequence converging in the neighborhood filter. |
addedSqueeze theoremb94ff1ed46ef
addedRatio test for series convergence2ee78d9aa0ef