sqrt_lt'

Mathlib.Data.Nat.Sqrt

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

English

For all m,n ∈ ℕ, sqrt m < n ↔ m < n^2.

Русский

Для всех m,n ∈ ℕ, sqrt m < n ↔ m < n^2.

LaTeX

$$$\sqrt{m} < n \iff m < n^2$$$

Lean4

theorem sqrt_lt' : sqrt m < n ↔ m < n ^ 2 := by simp only [← not_le, le_sqrt']

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

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

Разделы

Аффилиация

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