toBitVec_injective — Mathlib

English

The encoding map from 64-bit unsigned integers to 64-bit bit-vectors is one-to-one; if toBitVec(x) = toBitVec(y) then x = y.

Русский

Кодирующее отображение из 64-разрядных беззнаковых целых чисел в битовые векторы длины 64 является инъективным: если toBitVec(x) = toBitVec(y), то x = y.

LaTeX

$$$\\forall x,y \\in \\mathrm{UInt64}, \\operatorname{toBitVec}(x) = \\operatorname{toBitVec}(y) \\Rightarrow x = y$$$

Lean4

theorem toBitVec_injective : Function.Injective toBitVec :=
  @eq_of_toBitVec_eq

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