abs_coe_lt_top — Mathlib

English

Let x be a real number. When viewed inside the extended real line EReal, its absolute value remains finite, i.e., it is strictly below the top element.

Русский

Пусть x — действительное число. Рассматривая x как элемент расширенной вещественной прямой EReal, мы имеем, что |x| остаётся конечным: < верхняя граница топ.

LaTeX

$$$ \forall x \in \mathbb{R},\ (|x|_{EReal}) < \top $$$

Lean4

theorem abs_coe_lt_top (x : ℝ) : (x : EReal).abs < ⊤ :=
  ENNReal.ofReal_lt_top

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