nnreal_smul_lt_top

Mathlib.Data.ENNReal.Action

URI: https://scilib.ai/kg/mathlib#ENNReal.nnreal_smul_lt_top

English

If x ∈ NNReal and y ∈ ENNReal with y < ∞, then x • y < ∞.

Русский

Если x ∈ NNReal и y ∈ ENNReal с y < ∞, тогда x • y < ∞.

LaTeX

$$$ y < \infty \;\Rightarrow\; x \cdot y < \infty, \quad x \in \mathbb{R}_{\ge 0}. $$$

Lean4

theorem nnreal_smul_lt_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y < ⊤) : x • y < ⊤ :=
  mul_lt_top (by simp) hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru