isBoundedUnder_le_add — Mathlib

English

If u and v are f-bounded above (under ≤) and have the sum bounded, then u+v is f-bounded above.

Русский

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

LaTeX

$$$(\forall u,v,\ f.IsBoundedUnder(≤)\ u) \land (\ f.IsBoundedUnder(≤)\ v) \Rightarrow f.IsBoundedUnder(≤)(u+v)$$$

Lean4

theorem isBoundedUnder_le_add [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R}
    (u_bdd_le : f.IsBoundedUnder (· ≤ ·) u) (v_bdd_le : f.IsBoundedUnder (· ≤ ·) v) :
    f.IsBoundedUnder (· ≤ ·) (u + v) := by
  obtain ⟨U, hU⟩ := u_bdd_le
  obtain ⟨V, hV⟩ := v_bdd_le
  use U + V
  simp only [eventually_map, Pi.add_apply] at hU hV ⊢
  filter_upwards [hU, hV] with a hu hv using add_le_add hu hv

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