lt_sqrt

Mathlib.Data.Real.Sqrt

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

English

Let x,y ∈ ℝ with x ≥ 0. Then x < √y ⇔ x^2 < y.

Русский

Пусть x,y ∈ ℝ и x ≥ 0. Тогда x < √y ⇔ x^2 < y.

LaTeX

$$$\\\\forall x,y \\\\in \\\\mathbb{R}, x \\\\ge 0 \\\\Rightarrow (x < \\\\sqrt{y} \\\\iff x^2 < y)$$$

Lean4

theorem lt_sqrt (hx : 0 ≤ x) : x < √y ↔ x ^ 2 < y := by rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]

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

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

Разделы

Аффилиация

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