Structures · Topology

InfConvergenceClass

We say that α is an InfConvergenceClass if the following holds. Let f : ι → α be a monotone function, let a : α be a greatest lower bound of Set.range f. Then f x tends to 𝓝 a as x → -∞ (formally, at the filter Filter.atBot). We require this for ι = (s : Set α), f = (↑) in the definition, then prove it for any f in tendsto_atBot_isGLB. This property holds for linear orders with order topology as well as their products.

Defined in

Mathlib.Topology.Order.MonotoneConvergence

Shape

One type argument · adds tendsto_coe_atBot_isGLB