isBoundedUnder_of — Mathlib

English

A bounded function u: β → α yields that f is bounded under r if there exists b with r(u(x), b) for all x.

Русский

Если функция u: β → α ограничена относительно r, то фильтр f ограничен относительно r по границе b.

LaTeX

$$$$ (\exists b, \forall x, r(u(x),b)) \Rightarrow f.IsBoundedUnder r u $$$$

Lean4

/-- A bounded function `u` is in particular eventually bounded. -/
theorem isBoundedUnder_of {f : Filter β} {u : β → α} : (∃ b, ∀ x, r (u x) b) → f.IsBoundedUnder r u
  | ⟨b, hb⟩ => ⟨b, show ∀ᶠ x in f, r (u x) b from Eventually.of_forall hb⟩

Похожие утверждения