einfsep_le_of_mem_of_edist_le

Mathlib.Topology.MetricSpace.Infsep

URI: https://scilib.ai/kg/mathlib#Set.einfsep_le_of_mem_of_edist_le

← MathLib Explorer

English

If hx ∈ s, hy ∈ s, x ≠ y and edist x y ≤ d, then s.einfsep ≤ d.

Русский

Если x,y ∈ s, x ≠ y и edist x y ≤ d, тогда s.einfsep ≤ d.

LaTeX

$$$\text{If } x \in s, y \in s, x \neq y,\ edist x y \le d \Rightarrow s.einfsep \le d$$$

Lean4

theorem einfsep_le_of_mem_of_edist_le {d x} (hx : x ∈ s) {y} (hy : y ∈ s) (hxy : x ≠ y) (hxy' : edist x y ≤ d) :
    s.einfsep ≤ d :=
  le_trans (einfsep_le_edist_of_mem hx hy hxy) hxy'

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

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

Разделы

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

Аффилиация

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