sqrt_le_left

Mathlib.Data.Real.Sqrt

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

← MathLib Explorer

English

For y ≥ 0, √x ≤ y if and only if x ≤ y^2.

Русский

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

LaTeX

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

Lean4

theorem sqrt_le_left (hy : 0 ≤ y) : √x ≤ y ↔ x ≤ y ^ 2 := by
  rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]

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

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

Разделы

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

Аффилиация

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