bounded

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.bounded

English

Every CauSeq abv is bounded; there exists r such that abv(f i) < r for all i.

Русский

Каждая последовательность CauSeq abv ограничена сверху: существует r, такое что abv(f i) < r для всех i.

LaTeX

$$$\\exists r, \\forall i, abv(f i) < r$$$

Lean4

theorem bounded (f : CauSeq β abv) : ∃ r, ∀ i, abv (f i) < r :=
  f.2.bounded

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru