Metric (距離関数) (Section III.6)

• Metric (距離関数) (Section III.6) #Card
  • A function $d : X \times X \to \mathbb{R}_+$ is a metric on $X$ if for each $x, y, z \in X$: $d(x,y) = d(y,x)$; $d(x,y) = 0 \iff x = y$; $d(x,z) \leq d(x,y) + d(y,z)$.

Back

A function $d : X \times X \to \mathbb{R}_+$ is called a metric on $X$ if, for each $x, y, z \in X$, $$d(x,y) = d(y,x), \quad d(x,y) = 0 \iff x = y, \quad d(x,z) \leq d(x,y) + d(y,z).$$

（対称性・非退化性・三角不等式。値は非負実数。）

Lean

MetricSpace X（dist; 公理は dist_comm, dist_eq_zero, dist_triangle）