instMetricSpacePUnit — Mathlib

English

There is a canonical metric space structure on the one-point type PUnit.

Русский

Существует каноническая метрическая структура на единственном элементе PUnit.

LaTeX

$$MetricSpace PUnit$$

Lean4

instance : MetricSpace PUnit.{u + 1} 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 := by simp +contextual [principal_univ, eq_top_of_neBot (𝓤 PUnit)]

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