Theorems · Theorem · general topology

Filter.Tendsto.finSnoc

∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  {f : Y → (j : Fin n) → A j.castSucc} {g : Y → A (Fin.last n)} {l : Filter Y} {x : (j : Fin n) → A j.castSucc}
  {y : A (Fin.last n)},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun a => Fin.snoc (f a) (g a)) l (nhds (Fin.snoc x y))

Defined in

Mathlib.Topology.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace