limsup_top_eq_ciSup — Mathlib

English

If range u is bounded above and β is nonempty, then limsup u ⊤ equals the supremum of the values u(i).

Русский

Если диапазон u ограничен сверху и множество β непусто, то limsup u вверху равен наибольшему элементу {u(i)}.

LaTeX

$$$ \\operatorname{limsup} u \\top = \\bigvee_{i} u(i) $$$

Lean4

theorem limsup_top_eq_ciSup [Nonempty β] (hu : BddAbove (range u)) : limsup u ⊤ = ⨆ i, u i := by
  rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]

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