Theorems · Definition · general topology

Filter.limUnder

{X : Type u_1} → [TopologicalSpace X] → {α : Type u_3} → [Nonempty X] → Filter α → (α → X) → X

If f is a filter in α and g : α → X is a function, then Filter.limUnder f g is a limit of g at f, if it exists.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

47 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNonempty