liminf_top_eq_iInf

Mathlib.Order.LiminfLimsup

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

English

The liminf of the top filter equals the infimum of the range: liminf_top_eq_iInf.

Русский

Лиминф верхнего фильтра равен наименьшему значению из диапазона: liminf_top_eq_iInf.

LaTeX

$$$\\liminf(\\top) = \\inf_i u(i)$$$

Lean4

@[simp]
theorem liminf_top_eq_iInf (u : β → α) : liminf u ⊤ = ⨅ i, u i := by
  rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]

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

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

Разделы

Аффилиация

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