edist_le_diam_of_mem

Mathlib.Topology.EMetricSpace.Diam

URI: https://scilib.ai/kg/mathlib#EMetric.edist_le_diam_of_mem

← MathLib Explorer

English

If x and y lie in s, then edist(x, y) ≤ diam(s).

Русский

Если x и y принадлежат s, то edist(x, y) ≤ diam(s).

LaTeX

$$$(x \in s) \land (y \in s) \Rightarrow \operatorname{edist}(x, y) \le \operatorname{diam}(s)$$$

Lean4

/-- If two points belong to some set, their edistance is bounded by the diameter of the set -/
theorem edist_le_diam_of_mem (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s :=
  edist_le_of_diam_le hx hy le_rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru