sq_lt

Mathlib.Data.Real.Sqrt

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

English

For all x,y ∈ ℝ with y ≥ 0, x^2 < y iff -√y < x ∧ x < √y.

Русский

Пусть x,y ∈ ℝ и y ≥ 0. Тогда x^2 < y эквивалентно -√y < x < √y.

LaTeX

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

Lean4

theorem sq_lt : x ^ 2 < y ↔ -√y < x ∧ x < √y := by rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]

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

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

Разделы

Аффилиация

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