instOrderBot — Mathlib

English

The extended nonnegative real numbers carry a top element: there exists a greatest element for the natural order.

Русский

У расширенных неотрицательных вещественных чисел существует верхний элемент — наибольший элемент порядка.

LaTeX

$$$\forall x \in \mathbb{R}_{\ge 0}^\infty,\; x \le \top. $$$

Lean4

instance : OrderBot ℝ≥0∞ :=
  inferInstanceAs (OrderBot (WithTop ℝ≥0))

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