English
Let α be a complete lattice, p : ℕ → Prop, and u : ℕ → α. Then the blimsup of the sequence (u(n)) along the natural-atTop filter with predicate p equals ⨅ i ∈ ℕ, ⨆ {j ∈ ℕ | p(j) ∧ i ≤ j} u(j). In plain terms, blimsup u atTop p = inf_i sup_{j ≥ i, p(j)} u(j).
Русский
Пусть α — полная решетка, p : ℕ → Prop, и u : ℕ → α. Тогда блдимсуп последовательности (u(n)) по фильтру atTop с условием p равен ∞-мим инфimum по i: blimsup u atTop p = inf_{i} sup_{j ≥ i, p(j)} u(j).
LaTeX
$$$\\operatorname{blimsup} u\\, atTop\\, p = \\inf_{i \\in \\mathbb{N}} \\; \\sup_{\\substack{j \\ge i \\\\ p(j)}} u(j)$$$
Lean4
theorem blimsup_eq_iInf_biSup_of_nat {p : ℕ → Prop} {u : ℕ → α} :
blimsup u atTop p = ⨅ i, ⨆ (j) (_ : p j ∧ i ≤ j), u j := by
simp only [atTop_basis.blimsup_eq_iInf_iSup, @and_comm (p _), iSup_and, mem_Ici, iInf_true]
