sqrt_lt_sqrt_iff_of_pos

Mathlib.Data.Real.Sqrt

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

← MathLib Explorer

English

If y > 0, then √x < √y iff x < y.

Русский

Пусть y > 0. Тогда √x < √y эквивалентно x < y.

LaTeX

$$y > 0 \Rightarrow (\sqrt{x} < \sqrt{y} \iff x < y)$$

Lean4

theorem sqrt_lt_sqrt_iff_of_pos (hy : 0 < y) : √x < √y ↔ x < y := by
  rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]

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

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

Разделы

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

Аффилиация

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