instInf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance instInf : Min ℚ :=
  inferInstance

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