Zulip Chat Archive

Stream: maths

Topic: tendsto.nhds_congr


view this post on Zulip 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.

view this post on Zulip 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