English
If at least one of u or v is cobounded above along a linear order, then their pointwise maximum max(u, v) is cobounded above along the same filter.
Русский
Если хотя бы одна из функций u, v ограничена сверху вдоль линейного порядка, тогда их точечное максимумовое объединение max(u, v) также ограничено сверху вдоль того же фильтра.
LaTeX
$$$\text{If } f.\IsCoboundedUnder(≤) u \lor f.\IsCoboundedUnder(≤) v, \; f.\IsCoboundedUnder(≤) (\lambda a. \max(u(a), v(a)))$$$
Lean4
theorem isCoboundedUnder_le_max [LinearOrder β] {f : Filter α} {u v : α → β}
(h : f.IsCoboundedUnder (· ≤ ·) u ∨ f.IsCoboundedUnder (· ≤ ·) v) :
f.IsCoboundedUnder (· ≤ ·) (fun a ↦ max (u a) (v a)) := by
rcases h with (h' | h') <;>
· rcases h' with ⟨b, hb⟩
use b
intro c hc
apply hb c
rw [eventually_map] at hc ⊢
refine hc.mono (fun _ ↦ ?_)
simp +contextual only [implies_true, max_le_iff]
