divNatLtTwoPow — Mathlib

English

For n,d ∈ ℕ and e ∈ ℤ, the predicate compares n with d shifted by e if e ≥ 0, otherwise with d shifted by (−e − 1).

Русский

Для n,d ∈ ℕ и e ∈ ℤ предикат сравнивает n с d, смещённым на e, если e ≥ 0, иначе с d, смещённым на (−e − 1).

LaTeX

$$$\\text{divNatLtTwoPow}(n,d,e) = \\begin{cases} n < d \\cdot 2^{e} & \\text{if } e \\ge 0, \\\\ n \\cdot 2^{-(e+1)} < d & \\text{if } e < 0. \\end{cases}$$$

Lean4

@[nolint docBlame]
def divNatLtTwoPow (n d : ℕ) : ℤ → Bool
  | Int.ofNat e => n < d <<< e
  | Int.negSucc e => n <<< e.succ < d

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