linearGrowthSup_inv — Mathlib

English

The relation for negation of sequences: linearGrowthSup(-u) = - linearGrowthInf(u).

Русский

Отрицание последовательности в верхнем росте равносильно отрицанию нижнего роста: linearGrowthSup(-u) = - linearGrowthInf(u).

LaTeX

$$$\operatorname{linearGrowthSup}(-u) = -\operatorname{linearGrowthInf}(u)$$$

Lean4

theorem linearGrowthSup_inv : linearGrowthSup (-u) = -linearGrowthInf u :=
  by
  rw [linearGrowthInf, ← limsup_neg]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]

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