mul_le_left

Mathlib.Algebra.Order.Interval.Set.Instances

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

English

As above, for p ∈ Icc(0,1) and n ∈ ℕ, one has 0 ≤ p^n ≤ 1.

Русский

Как выше, для p ∈ Icc(0,1) и n ∈ ℕ верно 0 ≤ p^n ≤ 1.

LaTeX

$$0 ≤ (x^n) ≤ 1$$

Lean4

theorem mul_le_left {x y : Icc (0 : R) 1} : x * y ≤ x :=
  (mul_le_mul_of_nonneg_left y.2.2 x.2.1).trans_eq (mul_one _)

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

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

Разделы

Аффилиация

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