linearGrowthSup_congr — Mathlib

English

If two sequences u and v agree eventually, their upper linear growths are equal: linearGrowthSup(u) = linearGrowthSup(v).

Русский

Если две последовательности совпадают в дальнейшее время, их верхние темпы роста по линейной шкале равны.

LaTeX

$$$ \\text{linearGrowthSup} (u) = \\text{linearGrowthSup} (v) \\quad \\text{если } u =^\\infty v$$$

Lean4

theorem linearGrowthSup_congr (h : u =ᶠ[atTop] v) : linearGrowthSup u = linearGrowthSup v :=
  limsup_congr (h.mono fun _ uv ↦ uv ▸ rfl)

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