Theorems · Theorem · general topology

Filter.Tendsto.finInsertNth

∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  (i : Fin (n + 1)) {f : Y → A i} {g : Y → (j : Fin n) → A (i.succAbove j)} {l : Filter Y} {x : A i}
  {y : (j : Fin n) → A (i.succAbove j)},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun a => i.insertNth (f a) (g a)) l (nhds (i.insertNth 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