sqrt_lt'

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.sqrt_lt'

English

Let x,y ∈ ℝ with y > 0. Then √x < y iff x < y^2.

Русский

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

LaTeX

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

Lean4

theorem sqrt_lt' (hy : 0 < y) : √x < y ↔ x < y ^ 2 := by rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]

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

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

Разделы

Аффилиация

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