English
The bliminf (bounded liminf) of a function along a filter, bounded by p, is the supremum of a such that p(x) → u(x) ≥ a eventually holds.
Русский
Предел нижний обобщенный (bliminf) функции по фильтру, ограниченной предикатом p, есть supremum всех a, для которых p(x) → u(x) ≥ a выполняется для больших x.
LaTeX
$$$\operatorname{bliminf} (u,f,p) = \sup\{a : \forall^\infty x\in f,\ p(x) \to a ≤ u(x)\}$$$
Lean4
/-- 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. -/
def bliminf (u : β → α) (f : Filter β) (p : β → Prop) :=
sSup {a | ∀ᶠ x in f, p x → a ≤ u x}
