Theorems · Theorem · general topology

Filter.Tendsto.fst

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m : α → β × γ},
  Filter.Tendsto m f (g ×ˢ h) → Filter.Tendsto (fun a => (m a).1) f g

If a function tends to a product g ×ˢ h of filters, then its first component tends to g. See also Filter.Tendsto.fst_nhds for the special case of converging to a point in a product of two topological spaces.

Defined in

Mathlib.Order.Filter.Prod

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound