English
IsCobounded r f means there exists b such that for all a, if ∀ᶠ x in f, r x a then r b a.
Русский
IsCobounded r f означает, что существует b, так что для всех a: если ∀ᶠ x в f, r x a, тогда r b a.
LaTeX
$$$\mathrm{IsCobounded}\;r\;f \;\equiv\; \exists b, \forall a, (\forall^\mathrm{f} x \in f,\ r(x,a)) \rightarrow r(b,a).$$$
Lean4
/-- `IsCobounded (≺) f` states that the filter `f` does not tend to infinity w.r.t. `≺`. This is
also called frequently bounded. Will be usually instantiated with `≤` or `≥`.
There is a subtlety in this definition: we want `f.IsCobounded` to hold for any `f` in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
`¬ ∀ a, ∀ᶠ n in f, a ≤ n`
would not work as well in this case.
-/
def IsCobounded (r : α → α → Prop) (f : Filter α) :=
∃ b, ∀ a, (∀ᶠ x in f, r x a) → r b a
