isBounded_range

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#CauchySeq.isBounded_range

← MathLib Explorer

English

A Cauchy sequence has a bounded range.

Русский

Каунчаевой последовательности образ ограничен.

LaTeX

$$$CauchySeq\; f \Rightarrow IsBounded(\operatorname{range} f)$$$

Lean4

theorem _root_.CauchySeq.isBounded_range {f : ℕ → α} (hf : CauchySeq f) : IsBounded (range f) :=
  isBounded_range_of_cauchy_map_cofinite <| by rwa [Nat.cofinite_eq_atTop]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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