iSup_mul_le — Mathlib

English

For u, v : ι → ENNReal, ⨆ i, u_i · v_i ≤ (⨆ i, u_i) · (⨆ i, v_i).

Русский

Для функций u, v: ι → ENNReal справедливо неравенство верхнего предела: ⨆ i, u_i · v_i ≤ (⨆ i, u_i) · (⨆ i, v_i).

LaTeX

$$$\\displaystyle \\bigcup_i (u_i \\cdot v_i) \\leq \\left(\\sup_i u_i\\right) \\left(\\sup_i v_i\\right)$$$

Lean4

theorem iSup_mul_le {ι : Type*} {u v : ι → ℝ≥0∞} : ⨆ i, u i * v i ≤ (⨆ i, u i) * ⨆ i, v i :=
  iSup_le fun i ↦ mul_le_mul' (le_iSup u i) (le_iSup v i)

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