mul_le_right

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Icc.mul_le_right

English

For any x,y ∈ Icc(0,1), the product x·y is less than or equal to x.

Русский

Для любых x,y ∈ Icc(0,1) произведение x·y не превосходит x.

LaTeX

$$x\cdot y \le x$$

Lean4

theorem mul_le_right {x y : Icc (0 : R) 1} : x * y ≤ y :=
  (mul_le_mul_of_nonneg_right x.2.2 y.2.1).trans_eq (one_mul _)

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

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

Разделы

Аффилиация

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