Theorems · Theorem · general topology

tendsto_nhds_limUnder

∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {f : Filter α} {g : α → X}
  (h : ∃ x, Filter.Tendsto g f (nhds x)), Filter.Tendsto g f (nhds (f.limUnder g))

If g tends to some 𝓝 x along f, then it tends to 𝓝 (Filter.limUnder f g). We formulate this lemma with a [Nonempty X] argument of lim derived from h to make it useful for types without a [Nonempty X] instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance.

Defined in

Mathlib.Topology.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

TopologicalSpace