pow_four_le_pow_two_of_pow_two_le

Mathlib.Algebra.Order.Ring.Basic

URI: https://scilib.ai/kg/mathlib#pow_four_le_pow_two_of_pow_two_le

English

If a^2 ≤ b then a^4 ≤ b^2.

Русский

Если a^2 ≤ b, то a^4 ≤ b^2.

LaTeX

$$$a^2 \le b \Rightarrow a^4 \le b^2.$$$

Lean4

theorem pow_four_le_pow_two_of_pow_two_le {a b : R} (h : a ^ 2 ≤ b) : a ^ 4 ≤ b ^ 2 :=
  (pow_mul a 2 2).symm ▸ pow_le_pow_left₀ (sq_nonneg a) h 2

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

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

Разделы

Аффилиация

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