le_liminf_mul — Mathlib

English

For ENNReal sequences, limsup inequalities yield limsup of the product bounded by the product of limsups via a suitable ordering relation.

Русский

Для последовательностей ENNReal неравенства limsup приводят к ограничению limsup от произведения через произведение limsup.

LaTeX

$$$\limsup(u)\,\limsup(v) \geq \limsup(u\cdot v)$$$

Lean4

theorem le_liminf_mul : liminf u f * liminf v f ≤ liminf (u * v) f :=
  by
  refine mul_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (mul_lt_mul a_x b_x)

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