mul_le_right

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.mul_le_right

English

For x,y in unitInterval, x·y ≤ y.

Русский

Для любых x,y ∈ единичный интервал, x·y ≤ y.

LaTeX

$$$$ \forall x,y\in \text{unitInterval},\ x\cdot y \le y. $$$$

Lean4

theorem mul_le_right {x y : I} : x * y ≤ y :=
  Subtype.coe_le_coe.mp <| mul_le_of_le_one_left y.2.1 x.2.2

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

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

Разделы

Аффилиация

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