isCoboundedUnder_le_add — Mathlib

English

If u is f-bounded above and v is f-cobounded above, then u+v is f-bounded above.

Русский

Если u ограничен сверху по f, а v кобондированно ограничен сверху, то их сумма ограничена сверху по f.

LaTeX

$$$f.IsBoundedUnder(≤)\ u \rightarrow f.IsCoboundedUnder(≤)\ v \rightarrow f.IsCoboundedUnder(≤)\ (u+v)$$$

Lean4

theorem isCoboundedUnder_le_add (hu : f.IsBoundedUnder (· ≥ ·) u) (hv : f.IsCoboundedUnder (· ≤ ·) v) :
    f.IsCoboundedUnder (· ≤ ·) (u + v) := by
  obtain ⟨U, hU⟩ := hu.eventually_ge
  obtain ⟨V, hV⟩ := hv.frequently_ge
  apply IsCoboundedUnder.of_frequently_ge (a := U + V)
  exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Похожие утверждения