sqrt_le_sqrt

Mathlib.Data.Nat.Sqrt

URI: https://scilib.ai/kg/mathlib#Nat.sqrt_le_sqrt

English

If m ≤ n then sqrt m ≤ sqrt n.

Русский

Если m ≤ n, то sqrt m ≤ sqrt n.

LaTeX

$$[gcongr] $m \le n \Rightarrow \sqrt{m} \le \sqrt{n}$$$

Lean4

@[gcongr]
theorem sqrt_le_sqrt (h : m ≤ n) : sqrt m ≤ sqrt n :=
  le_sqrt.2 (le_trans (sqrt_le _) h)

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

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

Разделы

Аффилиация

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