instMetricSpaceEmpty — Mathlib

English

There exists a metric space structure on the empty type, where all distances are zero and the uniformity is trivial.

Русский

Существует метрическое пространство на пустом типе, где все расстояния равны нулю, а равномерная структура тривиальна.

LaTeX

$$MetricSpace Empty$$

Lean4

instance : MetricSpace Empty where
  dist _ _ := 0
  dist_self _ := rfl
  dist_comm _ _ := rfl
  edist _ _ := 0
  eq_of_dist_eq_zero _ := Subsingleton.elim _ _
  dist_triangle _ _ _ := show (0 : ℝ) ≤ 0 + 0 by rw [add_zero]
  toUniformSpace := inferInstance
  uniformity_dist := Subsingleton.elim _ _

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