liminf_add_le — Mathlib

English

In general, the liminf of the sum is at least the sum of liminfs.

Русский

В общем случае лиминф суммы не менее суммы лиминф.

LaTeX

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

Lean4

theorem liminf_add_le (h : limsup u f ≠ ⊥ ∨ liminf v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ liminf v f ≠ ⊥) :
    liminf (u + v) f ≤ (limsup u f) + (liminf v f) :=
  le_add_of_forall_gt h h' fun _ a_u _ b_v ↦
    (liminf_le_iff).2 fun _ c_ab ↦
      (((frequently_lt_of_liminf_lt) b_v).and_eventually ((eventually_lt_of_limsup_lt) a_u)).mono fun _ ab_x ↦
        (add_lt_add ab_x.2 ab_x.1).trans c_ab

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