Theorems · Definition · real analysis

Function.leftLim

{α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [TopologicalSpace β] → (α → β) → α → β

Let f : α → β be a function from a linear order α to a topological space β, and let a : α. The limit strictly to the left of f at a, denoted with leftLim f a, is defined by using the order topology on α. If a is isolated to its left or the function has no left limit, we use f a instead to guarantee a good behavior in most cases.

Defined in

Mathlib.Topology.Order.LeftRightLim

Cited by

60 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpace