emetricSpace — Mathlib

English

The map NonemptyCompacts.toCloseds is a uniform embedding.

Русский

Отображение NonemptyCompacts.toCloseds является равномерным вложением.

LaTeX

$$$\\text{IsUniformEmbedding} \\big(\\text{NonemptyCompacts.toCloseds}\\big).$$$

Lean4

/-- In emetric spaces, the Hausdorff edistance defines an emetric space structure
on the type of closed subsets -/
instance emetricSpace : EMetricSpace (Closeds α)
    where
  edist s t := hausdorffEdist (s : Set α) t
  edist_self _ := hausdorffEdist_self
  edist_comm _ _ := hausdorffEdist_comm
  edist_triangle _ _ _ := hausdorffEdist_triangle
  eq_of_edist_eq_zero {s t} h := Closeds.ext <| (hausdorffEdist_zero_iff_eq_of_closed s.isClosed t.isClosed).1 h

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