Theorems · Definition · order theory

Filter.bliminf

{α : Type u_1} → {β : Type u_2} → [ConditionallyCompleteLattice α] → (β → α) → Filter β → (β → Prop) → α

The bliminf of a function u along a filter f, bounded by a predicate p, is the supremum of the a such that the inequality a ≤ u x eventually holds for f whenever p x holds.

Defined in

Mathlib.Order.LiminfLimsup

Cited by

27 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLattice