isBoundedUnder_ge_add — Mathlib

English

If u and v are f-bounded below (under ≥), then their sum u+v is f-bounded below.

Русский

Если функции u и v ограничены снизу по отношению к фильтру f, то их сумма u+v также ограничена снизу.

LaTeX

$$$(\forall U,\ f.IsBoundedUnder(≥)\ u) \land (\forall V,\ f.IsBoundedUnder(≥)\ v) \Rightarrow f.IsBoundedUnder(≥)(u+v)$$$

Lean4

theorem isBoundedUnder_ge_add [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R}
    (u_bdd_ge : f.IsBoundedUnder (· ≥ ·) u) (v_bdd_ge : f.IsBoundedUnder (· ≥ ·) v) :
    f.IsBoundedUnder (· ≥ ·) (u + v) := by
  obtain ⟨U, hU⟩ := u_bdd_ge
  obtain ⟨V, hV⟩ := v_bdd_ge
  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

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