instMetricSpace — Mathlib

English

There is a metric space structure on Hamming β, obtained from the pseudo-metric space construction; i.e., Hamming β is a metric space under the defined distance.

Русский

Для пространства Хэмминга β существует метрическое пространство, полученное из конструкций псевдометрического пространства.

LaTeX

$$MetricSpace(Hamming β)$$

Lean4

instance : MetricSpace (Hamming β) :=
  .ofT0PseudoMetricSpace _

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