English
Let f be a filter on α, F : ι → α → β, s a finite set. If there exists i ∈ s such that F_i is cobounded above along f, then the Finset sup' is cobounded above as well.
Русский
Пусть f — фильтр на α, F : ι → α → β, s — конечное множество. Если существует i∈s such that F_i коб bounded по ≤ вдоль f, тогда sup' по s также кобbounded.
LaTeX
$$$\text{hs: } s.\Nonempty \\ (\exists i \in s, f.IsCoboundedUnder(≤)(F i)) \\Rightarrow f.IsCoboundedUnder(≤)(\lambda a. sup' s hs (\lambda i. F i a))$$$
Lean4
theorem isCoboundedUnder_le_finset_sup' [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty)
(h : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i)) : f.IsCoboundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a)) :=
by
rcases h with ⟨i, i_s, b, hb⟩
use b
refine fun c hc ↦ hb c ?_
rw [eventually_map] at hc ⊢
refine hc.mono fun a h ↦ ?_
simp only [sup'_le_iff] at h ⊢
exact h i i_s
