instSup — Mathlib

English

The rationals carry a binary maximum operation, i.e., there exists a well-defined 'max' on pairs of rationals which is greater than or equal to both arguments.

Русский

Рациональные числа имеют бинарную операцию максимума: существует функция max(a,b) такая, что max(a,b) ≥ a и max(a,b) ≥ b.

LaTeX

$$$\\max: \\mathbb{Q} \\times \\mathbb{Q} \\to \\mathbb{Q}$ exists with $a \\le \\max(a,b)$ and $b \\le \\max(a,b)$$$

Lean4

instance instSup : Max ℚ :=
  inferInstance

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