instSMulPosMonoNNReal

Mathlib.Data.ENNReal.Action

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

English

Let x ∈ NNReal and y ∈ ENNReal. If y ≠ ∞ then x • y ≠ ∞.

Русский

Пусть x ∈ NNReal и y ∈ ENNReal. Если y ≠ ∞, то x • y ≠ ∞.

LaTeX

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

Lean4

instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
  smul_le_smul_of_nonneg_right _r _ _a _b hab := mul_le_mul_right' (coe_le_coe.2 hab) _

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

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

Разделы

Аффилиация

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