Revision #1728 → #2230 · back to history
modifiedHeight of growing flower (continuous)ce8c02ec48db
| Field | From #1728 | To #2230 |
|---|
| note | This is an informal real-world illustration with no formal counterpart in Mathlib. | Informal real-world illustration with no formal counterpart in Mathlib. |
addedContinuity at isolated point is automatic6d152614bcaf
addedIVT corollary: sign change forces a zerodf36a9b94971
modifiedRight-continuous functionb387c0a274c9
| Field | From #1728 | To #2230 |
|---|
| note | Right-continuity is expressed as `ContinuousWithinAt f (Ici c) c`, with `continuousWithinAt_Ioi_iff_Ici` available. | Right-continuity is expressed as `ContinuousWithinAt f (Ici c) c`. |
addedPicard–Lindelöf theorem2d0452ef9769
modifiedQuotient topology (as final topology of surjection)93332c68ab08
| Field | From #1728 | To #2230 |
|---|
| mathlib.decl | Quotient.instTopologicalSpace | instTopologicalSpaceQuotient |
addedSubspace topology (initial topology of inclusion)62a9810833ef