English
If u is bounded above (≤) and v is cobounded below (≥) with respect to a filter and the underlying order supports addition, then u+v is cobounded below.
Русский
Если u ограничен сверху относительно фильтра, а v ограничен снизу, и порядок поддерживает сложение, то сумма u+v ограничена снизу.
LaTeX
$$$f.IsBoundedUnder(≤)\ u \land f.IsCoboundedUnder(≥)\ v \Rightarrow f.IsCoboundedUnder(≥)\ (u+v)$$$
Lean4
theorem isCoboundedUnder_ge_add (hu : f.IsBoundedUnder (· ≤ ·) u) (hv : f.IsCoboundedUnder (· ≥ ·) v) :
f.IsCoboundedUnder (· ≥ ·) (u + v) := by
obtain ⟨U, hU⟩ := hu.eventually_le
obtain ⟨V, hV⟩ := hv.frequently_le
apply IsCoboundedUnder.of_frequently_le (a := U + V)
exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1
