English
For a set of indices ι with a filter F on ι and a map a : ι → R, where R is a complete lattice, limsup a F equals the infimum over all I ∈ F.sets of the supremum over a(I).
Русский
Для множества индексов ι с фильтром F на ι и отображения a : ι → R, где R — полная решетка, limsup a F = inf_{I ∈ F.sets} sup(a(I)).
LaTeX
$$$\\displaystyle \\limsup a F = \\inf\\{ \\sup(a''I) : I \\in F.sets \\}$$$
Lean4
theorem limsup_eq_sInf_sSup {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) :
limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets) :=
by
apply le_antisymm
· rw [limsup_eq]
refine sInf_le_sInf fun x hx => ?_
rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
filter_upwards [I_mem_F] with i hi
exact hI ▸ le_sSup (mem_image_of_mem _ hi)
· refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_
rintro _ ⟨_, h, rfl⟩
exact h
