## Stream: maths

### Topic: tendsto.nhds_congr

#### Yury G. Kudryashov (Mar 03 2020 at 18:56):

Hi, do we have the following lemma somewhere in mathlib?

lemma tendsto.nhds_congr [uniform_space β] {l : filter α} {f g : α → β} {y : β}
(hf : tendsto f l (𝓝 y)) (hfg : tendsto (λ x, (f x, g x)) l (𝓤 β)) :
tendsto g l (𝓝 y) :=
sorry


I have a proof, just wonder if I should PR it, or use some existing lemma instead.

#### Yury G. Kudryashov (Mar 03 2020 at 18:57):

Probably this can be reformulated in terms of two filters on β without α.

Last updated: May 10 2021 at 08:14 UTC