mathlib3

5a3e8195 - feat(order/filter/basic): put pp_nodot attribute on filter.tendsto (#18062)

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`.