exists_lt_mul_self

Mathlib.Order.Filter.AtTopBot.Ring

URI: https://scilib.ai/kg/mathlib#exists_lt_mul_self

← MathLib Explorer

English

In a strict ordered ring, for every a there exists x ≥ 0 with a < x^2.

Русский

В строгом упорядоченном кольце для каждого a существует x ≥ 0 such that a < x^2.

LaTeX

$$$$\forall a \in R,\; \exists x \in R,\ x \ge 0 \land a < x^2.$$$$

Lean4

theorem exists_lt_mul_self (a : R) : ∃ x ≥ 0, a < x * x :=
  ((eventually_ge_atTop 0).and (tendsto_mul_self_atTop.eventually (eventually_gt_atTop a))).exists

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

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

Разделы

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

Аффилиация

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