sqrt_monotone

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.sqrt_monotone

English

The square root function is monotone: if x ≤ y, then √x ≤ √y.

Русский

Функция квадратного корня монотонна: если x ≤ y, то √x ≤ √y.

LaTeX

$$Monotone(Real.sqrt)$$

Lean4

theorem sqrt_monotone : Monotone Real.sqrt := fun _ _ ↦ sqrt_le_sqrt

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

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

Разделы

Аффилиация

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