le_limsup_mul — Mathlib

English

Under mild nondegeneracy assumptions, limsup(u·v) ≤ limsup(u)·limsup(v).

Русский

При разумных предположениях неравенств, limsup(u·v) ≤ limsup(u)·limsup(v).

LaTeX

$$$\limsup (u\cdot v) \leq \limsup u \cdot \limsup v$$$

Lean4

theorem le_limsup_mul : limsup u f * liminf v f ≤ limsup (u * v) f :=
  mul_le_of_forall_lt fun a a_u b b_v ↦
    (le_limsup_iff).2 fun c c_ab ↦
      Frequently.mono (Frequently.and_eventually ((frequently_lt_of_lt_limsup) a_u) ((eventually_lt_of_lt_liminf) b_v))
        fun _ ab_x ↦ c_ab.trans (mul_lt_mul ab_x.1 ab_x.2)

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