English
For a given e ∈ ℤ and m ∈ ℕ, the pair (e, m) is valid finite if emin ≤ e + prec − 1, e + prec − 1 ≤ emax, and e = max(e + m.size − prec, emin).
Русский
Для заданных e ∈ ℤ и m ∈ ℕ пара (e,m) допустима как конечная, если выполняются неравенства: emin ≤ e + prec − 1 и e + prec − 1 ≤ emax, и e = max(e + m.size − prec, emin).
LaTeX
$$$\\mathrm{ValidFinite}(e,m) \\iff (\\mathrm{emin} \\le e + \\mathrm{prec} - 1) \\land (e + \\mathrm{prec} - 1 \\le \\mathrm{emax}) \\land \\left( e = \\max\\left(e + m.\\mathrm{size} - \\mathrm{prec}, \\mathrm{emin}\\right) \\right)$$$
Lean4
@[nolint docBlame]
def ValidFinite (e : ℤ) (m : ℕ) : Prop :=
emin ≤ e + prec - 1 ∧ e + prec - 1 ≤ emax ∧ e = max (e + m.size - prec) emin
