Theorems · Definition · order theory

Filter.blimsup

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

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

Defined in

Mathlib.Order.LiminfLimsup

Cited by

40 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLattice