English
Let f be a filter on α, F : ι → α → β, and s a nonempty finite set of indices. If each F_i is bounded above along f, then the Finset sup' across i ∈ s is also bounded above along f.
Русский
Пусть f — фильтр на α, F : ι → α → β, и s — непустое конечное множество индексов. Если каждый F_i ограничен сверху вдоль f, то Finset sup' по i∈s тоже ограничен сверху вдоль f.
LaTeX
$$$\text{hs: } s.\Nonempty \\ (\forall i \in s,\; f.IsBoundedUnder(≤)(F i)) \Rightarrow f.IsBoundedUnder(≤)(\lambda a. sup' s hs (\lambda i. F i a))$$$
Lean4
theorem isBoundedUnder_le_finset_sup' [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
(hs : s.Nonempty) (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) :
f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a)) :=
by
choose! m hm using h
use sup' s hs m
simp only [eventually_map] at hm ⊢
rw [← eventually_all_finset s] at hm
refine hm.mono fun a h ↦ ?_
simp only [sup'_le_iff]
exact fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)
