le_liminf_add — Mathlib

English

The sum of liminfs is at most the liminf of the pointwise sum.

Русский

Сумма liminf не превосходит liminf от поэлементной суммы.

LaTeX

$$$ (\liminf u) + (\liminf v) \le \liminf (u+v) $$$

Lean4

theorem le_liminf_add : (liminf u f) + (liminf v f) ≤ liminf (u + v) f :=
  by
  refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (add_lt_add a_x b_x)

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