Revision #2344 → #3480 · back to history
c212b42f922a| Field | From #2344 | To #3480 |
|---|---|---|
| mathlib.decl | analyticAt_sigmoid | Real.analyticAt_sigmoid |
| note | `analyticAt_sigmoid` (and `analyticOnNhd_sigmoid` on `Set.univ`) prove sigmoid is real-analytic everywhere. | `Real.analyticAt_sigmoid` (and `Real.analyticOnNhd_sigmoid` on `Set.univ`) prove sigmoid is real-analytic everywhere. |