Revision #1960 → #2382 · back to history
modifiedLimit of 4x+1 at x=20cd8765320cf
| Field | From #1960 | To #2382 |
|---|
| note | This is a worked numerical example, not a named theorem; no dedicated Mathlib statement was located. | Worked numerical example, not a named theorem; no dedicated Mathlib statement located. |
modifiedLimit independent of value at p1e648b21e6f8
| Field | From #1960 | To #2382 |
|---|
| note | Mathlib's `𝓝[≠] p` filter encodes the deleted neighborhood used to ignore `f p`, but the article's specific example itself is not formalized. | Mathlib's `𝓝[≠] p` filter (built from `nhdsWithin`) encodes the deleted neighborhood used to ignore `f p`, but the article's specific example itself is not formalized. |
modifiedWhere limits can existf10056af019e
| Field | From #1960 | To #2382 |
|---|
| note | Mathlib uses `(𝓝[s \ {p}] p).NeBot` (cluster-point conditions) for the analogous existence requirement, but the article's exact closure/interior-based statement is not stated as a single lemma. | Mathlib uses `(𝓝[s \ {p}] p).NeBot` (cluster-point conditions) for the analogous existence requirement, but the article's exact closure/interior-based statement is not a single named lemma. |
modifiedRight-handed limit07fd91316c99
| Field | From #1960 | To #2382 |
|---|
| note | `Function.rightLim` and `Tendsto f (𝓝[>] p) (𝓝 L)` (with `nhdsGT` notation in `Mathlib.Topology.Defs.Filter`) capture the right-handed limit. | `Function.rightLim` and `Tendsto f (𝓝[>] p) (𝓝 L)` capture the right-handed limit. |
modifiedNon-existence implies non-zero oscillationfd8c5641d4a1
| Field | From #1960 | To #2382 |
|---|
| mathlib.decl | eq_zero_iff_continuousAt | Oscillation.eq_zero_iff_continuousAt |
modifiedLimit as x approaches infinity82337ce98a87
| Field | From #1960 | To #2382 |
|---|
| mathlib.module | Mathlib.Order.Filter.AtTopBot.Basic | Mathlib.Order.Filter.AtTopBot.Defs |
modifiedLimit as x approaches minus infinity52c385f074b6
| Field | From #1960 | To #2382 |
|---|
| mathlib.module | Mathlib.Order.Filter.AtTopBot.Basic | Mathlib.Order.Filter.AtTopBot.Defs |
modifiedLimit at −∞ of exponential decayab1a6d4ec615
| Field | From #1960 | To #2382 |
|---|
| note | Specific worked example; the general limit `Real.tendsto_exp_atBot` is in Mathlib but this exact computation is not. | Specific worked example; the general limit `Real.tendsto_exp_atBot` exists but this exact computation does not. |
modifiedDouble (multiple) limit87d451fd6c88
| Field | From #1960 | To #2382 |
|---|
| mathlib.decl | Filter.prod | Filter.instSProd |
| mathlib.module | Mathlib.Order.Filter.Prod | Mathlib.Order.Filter.Defs |
| note | The double/multiple limit is `Tendsto f (𝓝 p ×ˢ 𝓝 q) (𝓝 L)` using the product `Filter.prod`. | The double/multiple limit is `Tendsto f (𝓝 p ×ˢ 𝓝 q) (𝓝 L)`, with the product filter supplied by `Filter.instSProd`. |
modifiedDouble limit at +∞e01e24e15cae
| Field | From #1960 | To #2382 |
|---|
| mathlib.decl | Filter.prod | Filter.instSProd |
| mathlib.module | Mathlib.Order.Filter.Prod | Mathlib.Order.Filter.Defs |
| note | Expressed as `Tendsto f (atTop ×ˢ atTop) (𝓝 L)`. | Expressed as `Tendsto f (atTop ×ˢ atTop) (𝓝 L)` via the product filter from `Filter.instSProd`. |
modifiedDouble limit at −∞01295098304b
| Field | From #1960 | To #2382 |
|---|
| mathlib.decl | Filter.prod | Filter.instSProd |
| mathlib.module | Mathlib.Order.Filter.Prod | Mathlib.Order.Filter.Defs |
| note | Expressed as `Tendsto f (atBot ×ˢ atBot) (𝓝 L)`. | Expressed as `Tendsto f (atBot ×ˢ atBot) (𝓝 L)` via the product filter from `Filter.instSProd`. |
modifiedLimit of a vector-valued function (Euclidean)208e5734c7dc
| Field | From #1960 | To #2382 |
|---|
| mathlib.module | Mathlib.Analysis.InnerProductSpace.EuclideanDist | Mathlib.Analysis.InnerProductSpace.PiL2 |
modifiedLimit under the Manhattan metric0619e3985ff1
| Field | From #1960 | To #2382 |
|---|
| note | `PiLp 1 fun i => ℝ` is the Manhattan metric instance; convergence reduces (via `PiLp.equiv`) to the usual product convergence. | `PiLp 1 fun i => ℝ` provides the Manhattan (L¹) metric instance; convergence reduces to the usual product convergence. |
addedIndeterminate forms212d4ebb9ad4
addedUniqueness of limit in Hausdorff space82f2de18e71f
addedContinuity at limit point characterized by limit3504161dd3e1