toHamming — Mathlib

English

There is a canonical equivalence between the function space ∀ i, β i and Hamming β given by the identity map.

Русский

Существует каноническое эквивалентное отображение между пространством функций ∀ i, β i и Hamming β, заданное идентичностью.

LaTeX

$$$(\forall i, \beta i) \simeq Hamming(\beta)$$$

Lean4

/-- `Hamming.toHamming` is the identity function to the `Hamming` of a type. -/
@[match_pattern]
def toHamming : (∀ i, β i) ≃ Hamming β :=
  Equiv.refl _

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