English
Let M be an Archimedean ordered group with addition, and a distinguished 1. There is a real-valued map embedRealFun from M to the reals defined by taking the supremum of all rational numbers strictly below x. This provides a way to view elements of M inside ℝ via their rational lower bounds.
Русский
Пусть M — упорядоченная абелева группа с сложением и единицей, удовлетворяющая условию Архимедея. Существует отображение embedRealFun: M → ℝ, задаваемое как наибольшая нижняя рациональная оценка элемента x, то есть embedRealFun(x) = sup{ q ∈ ℚ : q < x }. Оно задаёт отображение элементов M в ℝ через рациональные приближения снизу.
LaTeX
$$$\operatorname{embedRealFun}(x) = \sup \{ q \in \mathbb{Q} : q < x \}$$$
Lean4
/-- Mapping `M` to `ℝ`, defined as the supremum of `ratLt' x`. -/
noncomputable abbrev embedRealFun (x : M) :=
sSup (ratLt' x)
