Revision #2601 → #3193 · back to history
modifiedSubsequential limitb84447b64d25
| Field | From #2601 | To #3193 |
|---|
| mathlib.module | Mathlib.Topology.ClusterPt | Mathlib.Topology.Defs.Filter |
modifiedSubadditivity of limit superiorcee4f2831e9c
| Field | From #2601 | To #3193 |
|---|
| note | `Filter.limsup_add_le` proves `limsup (u + v) ≤ limsup u + limsup v`. | `limsup_add_le` (bare, in the root namespace) proves `limsup (u + v) f ≤ limsup u f + limsup v f` on a suitable ordered add-comm group. |
modifiedSuperadditivity of limit inferiord034c2233650
| Field | From #2601 | To #3193 |
|---|
| note | `Filter.le_liminf_add` proves `liminf u + liminf v ≤ liminf (u + v)`. | `le_liminf_add` proves `liminf u f + liminf v f ≤ liminf (u + v) f` (root namespace, not under `Filter`). |
modifiedMultiplicative inequalities for non-negative sequences4b03c6e41f54
| Field | From #2601 | To #3193 |
|---|
| note | `Filter.limsup_mul_le`, `Filter.le_liminf_mul`, and `Filter.liminf_mul_le` provide the multiplicative analogues for non-negative functions. | `limsup_mul_le`, `le_liminf_mul`, and `liminf_mul_le` (root namespace) provide the multiplicative analogues for eventually non-negative real-valued functions. |
modifiedDiscrete metricdfa0706a47f8
| Field | From #2601 | To #3193 |
|---|
| mathlib.module | Mathlib.Topology.Defs.Basic | Mathlib.Topology.Order |
modifiedCluster points of a filter base8c299eb79b88
| Field | From #2601 | To #3193 |
|---|
| mathlib.module | Mathlib.Topology.ClusterPt | Mathlib.Topology.Defs.Filter |
addedExtended real line is a complete lattice731de1d4f921
addedNegation swaps limsup and liminfac3bc01258e3
addedInf and sup bound liminf and limsup328b8684cb9b