Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-05 07:04 5a3e8195

View on Github →

feat(order/filter/basic): put pp_nodot attribute on filter.tendsto (#18062) Make sure that tendsto f p q is not pretty-printed as p.tendsto f q, since this is not a property of p but rather of f.

Estimated changes