le_edist_of_le_einfsep

Mathlib.Topology.MetricSpace.Infsep

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\text{If } hx:\, x \in s, hy:\, y \in s, hxy:\, x \neq y, and hd:\, d \le s.einfsep,\ \text{then } d \le edist x y.$$$

Lean4

theorem le_edist_of_le_einfsep {d x} (hx : x ∈ s) {y} (hy : y ∈ s) (hxy : x ≠ y) (hd : d ≤ s.einfsep) : d ≤ edist x y :=
  le_einfsep_iff.1 hd x hx y hy hxy

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

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

Разделы

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

Аффилиация

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