Theorems · Theorem · general topology

Filter.Tendsto.fst_nhds

∀ {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {X : Type u_5} {l : Filter X}
  {f : X → Y × Z} {p : Y × Z}, Filter.Tendsto f l (nhds p) → Filter.Tendsto (fun a => (f a).1) l (nhds p.1)

Defined in

Mathlib.Topology.Constructions.SumProd

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace