fst_eq_of_dist_lt_one

Mathlib.Topology.MetricSpace.Gluing

URI: https://scilib.ai/kg/mathlib#Metric.Sigma.fst_eq_of_dist_lt_one

English

If the distance between two points is less than 1, then their indices are equal.

Русский

Если расстояние между двумя точками меньше 1, то их индексы равны.

LaTeX

$$$\forall x,y,\; \mathrm{dist}(x,y) < 1 \Rightarrow x.1 = y.1$$$

Lean4

theorem fst_eq_of_dist_lt_one (x y : Σ i, E i) (h : dist x y < 1) : x.1 = y.1 :=
  by
  cases x; cases y
  contrapose! h
  apply one_le_dist_of_ne h

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

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

Разделы

Аффилиация

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