eq_of_hammingDist_eq_zero — Mathlib

English

Equality of functions follows from zero distance by the auxiliary lemma.

Русский

Равенство функций следует из нулевого расстояния по вспомогательной лемме.

LaTeX

$$eq_of_hammingDist_eq_zero {x y} (h : hammingDist x y = 0) : x = y$$

Lean4

/-- Corresponds to `eq_of_dist_eq_zero`. -/
theorem eq_of_hammingDist_eq_zero {x y : ∀ i, β i} : hammingDist x y = 0 → x = y := by
  simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ, forall_true_left,
    imp_self]

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