eq_of_forall_dist_le

Mathlib.Topology.MetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#eq_of_forall_dist_le

← MathLib Explorer

English

If the distance between x and y is smaller than every positive real number, then x = y.

Русский

Если расстояние между x и y меньше любого положительного числа ε > 0, то x = y.

LaTeX

$$(forall ε > 0, dist\ x\ y ≤ ε) → x = y$$

Lean4

theorem eq_of_forall_dist_le {x y : γ} (h : ∀ ε > 0, dist x y ≤ ε) : x = y :=
  eq_of_dist_eq_zero (eq_of_le_of_forall_lt_imp_le_of_dense dist_nonneg h)

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

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

Разделы

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

Аффилиация

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