toFin_injective

Mathlib.Data.UInt

URI: https://scilib.ai/kg/mathlib#UInt8.toFin_injective

English

The function toFin on 8-bit unsigned integers is injective.

Русский

Функция toFin на 8-битных беззнаковых целых числах инъективна.

LaTeX

$$$\mathrm{toFin}:\mathrm{UInt8} \to \mathrm{Fin}\;256\;\text{ is injective}$$$

Lean4

theorem toFin_injective : Function.Injective toFin :=
  @eq_of_toFin_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru