linearGrowthInf_neg — Mathlib

English

The relation between infimum and supremum under negation: linearGrowthInf(-u) = - linearGrowthSup(u).

Русский

Соотношение инф в отрицании: linearGrowthInf(-u) = - linearGrowthSup(u).

LaTeX

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

Lean4

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

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