chore: improve docstring of pipe operators

[jcreedcmu]

A minor documentation improvement. It is possible for a user to write x |> .f when they meant x |>.f or vice-versa and it's helpful to be informed of the alternative on hover.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 917715c86225aeb2f0da13885acb9becb0ee79ef --onto d869c38e7bee7d484040b758837be76f55db9498. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-16 15:05:52)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 917715c86225aeb2f0da13885acb9becb0ee79ef --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-16 15:05:54)

[david-christiansen]

This is a strict improvement as-is.

However, while you're at it, perhaps something like this this would be good too?

Suggested change

	Haskell-like pipe operator `|>`. `x |> f` means the same as `f x`,
	and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
	The pipe operator `|>`, which allows a function to be placed _after_ its argument.
	`x |> f` is equivalent to `f x`, and it chains such that `x |> f |> g` is interpreted as `g (f x)`. This
	directs readers' attention to an initial value and a sequence of transformations, instead of
	centering the function.

This operator is not widely used in Haskell, where & is more common for this purpose. It's certainly very common in F#, and I believe it's also popular in many Haskell-derived languages. I think it's also useful to point out why someone might want to write the argument before the function.