ofHamming_toHamming — Mathlib

English

The encoding from a family of objects x = (x i) to its Hamming representation has the inverse x ↦ toHamming x, and decoding recovers the original family; i.e., ofHamming (toHamming x) = x for all x.

Русский

Кодирование семейства объектов x = (x_i) в представление Хэмминга имеет обратное преобразование; расшифровка восстанавливает исходное семейство: for all x, ofHamming (toHamming x) = x.

LaTeX

$$$\\operatorname{ofHamming}(\\operatorname{toHamming} x) = x$$$

Lean4

@[simp]
theorem ofHamming_toHamming (x : ∀ i, β i) : ofHamming (toHamming x) = x :=
  rfl

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