diam_closure — Mathlib

English

The diameter of a set is unchanged when passing to its closure in an emetric space.

Русский

Диаметр множества не меняется при переходе к его замыканию в эметрическом пространстве.

LaTeX

$$$\operatorname{diam}(\overline{S}) = \operatorname{diam}(S)$ for any set S.$$

Lean4

@[simp]
theorem diam_closure (s : Set α) : diam (closure s) = diam s :=
  by
  refine le_antisymm (diam_le fun x hx y hy => ?_) (diam_mono subset_closure)
  have : edist x y ∈ closure (Iic (diam s)) :=
    map_mem_closure₂ continuous_edist hx hy fun x hx y hy => edist_le_diam_of_mem hx hy
  rwa [closure_Iic] at this

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