English
If there exists a point a in α such that for every set s in the filter f there exists x ∈ s with r(a,x), then f is cobounded with respect to r.
Русский
Если существует точка a в α такая, что для каждого множества s в фильтре f существует x ∈ s с свойством r(a,x), то фильтр f является cobounded по отношению r.
LaTeX
$$$\exists a \in α, \forall s \in f, \exists x \in s, r(a,x) \Rightarrow f.IsCobounded r.$$$
Lean4
/-- To check that a filter is frequently bounded, it suffices to have a witness
which bounds `f` at some point for every admissible set.
This is only an implication, as the other direction is wrong for the trivial filter. -/
theorem mk [IsTrans α r] (a : α) (h : ∀ s ∈ f, ∃ x ∈ s, r a x) : f.IsCobounded r :=
⟨a, fun _ s =>
let ⟨_, h₁, h₂⟩ := h _ s
_root_.trans h₂ h₁⟩
