limsup_top_eq_iSup

Mathlib.Order.LiminfLimsup

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

English

The limsup of the top filter equals the supremum over the range: limsSup_top_eq_iSup u.

Русский

Лимсуп верхнего фильтра равен объединению по диапазону: limsup_top_eq_iSup u

LaTeX

$$$\\limsup\\,u\\top = \\big\\uplus_i u(i)\\!$$$

Lean4

@[simp]
theorem limsup_top_eq_iSup (u : β → α) : limsup u ⊤ = ⨆ i, u i := by
  rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]

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

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

Разделы

Аффилиация

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