hammingDist_le_card_fintype — Mathlib

English

The distance between two functions over a finite index set is at most the cardinality of that index set.

Русский

Расстояние между двумя функциями по конечному индексу не превосходит кардинальности этого множества индексов.

LaTeX

$$hammingDist(x,y) ≤ Fintype.card ι$$

Lean4

theorem hammingDist_le_card_fintype {x y : ∀ i, β i} : hammingDist x y ≤ Fintype.card ι :=
  card_le_univ _

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