English
If for every i in a finite set s, F_i is bounded above, then the function a ↦ sup s (F i a) is bounded above along the filter.
Русский
Если для каждого i из конечного множества s функция F_i ограничена сверху, то функция a ↦ sup s (F_i(a)) ограничена сверху вдоль фильтра.
LaTeX
$$$\forall i\in s,\; f.IsBoundedUnder(≤)(F i) \Rightarrow f.IsBoundedUnder(≤)(\lambda a. sup s (\lambda i. F i a))$$$
Lean4
theorem isBoundedUnder_le_finset_sup [LinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
(h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) : f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup s (fun i ↦ F i a)) :=
by
choose! m hm using h
use sup s m
simp only [eventually_map] at hm ⊢
rw [← eventually_all_finset s] at hm
exact hm.mono fun _ h ↦ sup_mono_fun h
