mul_le_left

Mathlib.Topology.UnitInterval

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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