limsup_add_le — Mathlib

English

The limsup of a sum is bounded above by the sum of limsup: f.limsup (u + v) ≤ f.limsup u + f.limsup v.

Русский

Предел верхний суммы не превосходит суммы пределов верхних: limsup (u+v) ≤ limsup u + limsup v.

LaTeX

$$$\\\\forall f : \\text{Filter } α [CountableInterFilter f] (u v : α \\\\to \\\\mathbb{R}_{\\\\ge 0,\\\\infty}), \\\\; f.limsup (u + v) \\\\le f.limsup u + f.limsup v$$$

Lean4

theorem limsup_add_le [CountableInterFilter f] (u v : α → ℝ≥0∞) : f.limsup (u + v) ≤ f.limsup u + f.limsup v :=
  sInf_le ((eventually_le_limsup u).mp ((eventually_le_limsup v).mono fun _ hxg hxf => add_le_add hxf hxg))

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