Filter.Tendsto.fst

Stream: Is there code for X?

[Anatole Dedecker]

I could have sworn we had something like this:

lemma Filter.Tendsto.fst {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] {l : Filter Z}
    {f : Z → X × Y} {x : X} {y : Y} (H : Tendsto f l (𝓝 (x, y))) : Tendsto (Prod.fst ∘ f) l (𝓝 x) :=
  continuous_fst.tendsto _ |>.comp H

Am I missing something? Do we not want this for some reason?

[Yury G. Kudryashov]

We have docs#Continuous.fst. As for this lemma, it should mention nhds somewhere in its name, because Filter.Tendsto.fst should be about the product of 2 filters, not nhds.

[Anatole Dedecker]

Yes I agree. And I guess we should also add the docs#Filter.pi version of docs#Filter.Tendsto.apply ?

[Yury G. Kudryashov]

Yes, Tendsto.apply was there before we added Filter.pi.

[Anatole Dedecker]

#11812