toNNRat — Mathlib

English

A rational number q is reinterpreted as a nonnegative rational by taking the maximum with 0: toNNRat(q) = ⟨max(q,0), proof⟩.

Русский

Рациональное число q интерпретируется как неотрицательное рациональное число через max(q,0): toNNRat(q) = ⟨max(q,0), доказательство⟩.

LaTeX

$$$\operatorname{toNNRat}(q) = \langle \max(q,0), \text{proof} \rangle$$$

Lean4

/-- Reinterpret a rational number `q` as a non-negative rational number. Returns `0` if `q ≤ 0`. -/
def _root_.Rat.toNNRat (q : ℚ) : ℚ≥0 :=
  ⟨max q 0, le_max_right _ _⟩

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