liminf_eq_iSup_iInf_of_nat

Mathlib.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#Filter.liminf_eq_iSup_iInf_of_nat

English

Let u : ℕ → α. Then liminf u atTop = ⨆ n : ℕ, ⨅ i, u(i + n).

Русский

Пусть u : ℕ → α. Тогда лиминф по atTop равен ⨆ n, ⨅ i, u(i + n).

LaTeX

$$$\\displaystyle \\liminf u\\ atTop = \\big\\!\\sup_{n \\in \\mathbb{N}} \\bigl(\\inf_{i \\in \\mathbb{N}} u(i + n)\\bigr)$$$

Lean4

theorem liminf_eq_iSup_iInf_of_nat {u : ℕ → α} : liminf u atTop = ⨆ n : ℕ, ⨅ i ≥ n, u i :=
  @limsup_eq_iInf_iSup_of_nat αᵒᵈ _ u

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

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

Разделы

Аффилиация

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