metricSpace — Mathlib

English

The p-adic numbers form a metric space with distance d(x,y) = |x - y|_p.

Русский

p-адические числа образуют метрическое пространство с расстоянием d(x,y) = |x - y|_p.

LaTeX

$$$\mathbb{Q}_p \text{ is a metric space with } d(x,y) = |x - y|_p$$$

Lean4

instance metricSpace : MetricSpace ℚ_[p] where
  dist_self := by simp [dist]
  dist := dist
  dist_comm x y := by simp [dist, ← padicNormE.map_neg (x - y : ℚ_[p])]
  dist_triangle x y
    z := by
    dsimp [dist]
    exact mod_cast padicNormE.sub_le x y z
  eq_of_dist_eq_zero := by
    dsimp [dist]; intro _ _ h
    apply eq_of_sub_eq_zero
    apply padicNormE.eq_zero.1
    exact mod_cast h

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