Revision #1361 → #2601 · back to history
modifiedSubadditivity of limit superiorcee4f2831e9c
| Field | From #1361 | To #2601 |
|---|
| mathlib.decl | Filter.limsup_add_le | limsup_add_le |
| provenance | ai | ai-moderated |
modifiedSuperadditivity of limit inferiord034c2233650
| Field | From #1361 | To #2601 |
|---|
| mathlib.decl | Filter.le_liminf_add | le_liminf_add |
| provenance | ai | ai-moderated |
modifiedMultiplicative inequalities for non-negative sequences4b03c6e41f54
| Field | From #1361 | To #2601 |
|---|
| mathlib.decl | Filter.limsup_mul_le | limsup_mul_le |
| provenance | ai | ai-moderated |
modifiedReformulation via sequences1c2d09dc6196
| Field | From #1361 | To #2601 |
|---|
| mathlib.decl | Filter.exists_seq_tendsto_limsup | exists_seq_tendsto_limsup |
| provenance | ai | ai-moderated |