sq_le

Mathlib.Data.Real.Sqrt

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

← MathLib Explorer

English

For y ≥ 0, x^2 ≤ y iff -√y ≤ x ≤ √y.

Русский

Для y ≥ 0 верно: x^2 ≤ y эквивалентно -√y ≤ x ≤ √y.

LaTeX

$$$y \ge 0 \Rightarrow (x^2 \le y \iff -\sqrt{y} \le x \land x \le \sqrt{y})$$$

Lean4

theorem sq_le (h : 0 ≤ y) : x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y :=
  by
  constructor
  · simpa only [abs_le] using abs_le_sqrt
  · rw [← abs_le, ← sq_abs]
    exact (le_sqrt (abs_nonneg x) h).mp

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

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

Разделы

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

Аффилиация

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