Commit 2024-03-31 21:48 64528268

feat: add Tendsto.fst, Tendsto.snd, Tendsto.apply and nhds versions (#11812)

• Add Tendsto.fst, Tendsto.snd and Tendsto.apply (these are about product of filters)
• Move the current Tendsto.apply to Tendsto.apply_nhds, and add Tendsto.fst_nhds and Tendsto.snd_nhds (these are about neighborhoods in a product space)