sqLe_of_le

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.sqLe_of_le

← MathLib Explorer

English

If z ≤ x and y ≤ w and SqLe x c y d, then SqLe z c w d.

Русский

Если z ≤ x и y ≤ w и SqLe x c y d, тогда SqLe z c w d.

LaTeX

$$$ z \le x \rightarrow y \le w \rightarrow SqLe(x,c,y,d) \rightarrow SqLe(z,c,w,d)$$$

Lean4

theorem sqLe_of_le {c d x y z w : ℕ} (xz : z ≤ x) (yw : y ≤ w) (xy : SqLe x c y d) : SqLe z c w d :=
  calc
    c * z * z ≤ c * x * x := by gcongr
    _ ≤ d * y * y := xy
    _ ≤ d * w * w := by gcongr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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