diam_mono

Mathlib.Topology.EMetricSpace.Diam

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

← MathLib Explorer

English

If s ⊆ t, then diam(s) ≤ diam(t).

Русский

Если s ⊆ t, то diam(s) ≤ diam(t).

LaTeX

$$\text{If } s \subseteq t, \quad \operatorname{diam}(s) \le \operatorname{diam}(t)$$

Lean4

/-- The diameter is monotonous with respect to inclusion -/
@[gcongr]
theorem diam_mono {s t : Set α} (h : s ⊆ t) : diam s ≤ diam t :=
  diam_le fun _x hx _y hy => edist_le_diam_of_mem (h hx) (h hy)

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

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

Разделы

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

Аффилиация

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