embeddingOfSubset_coe

Mathlib.Topology.MetricSpace.Kuratowski

URI: https://scilib.ai/kg/mathlib#KuratowskiEmbedding.embeddingOfSubset_coe

English

The nth coordinate of the Kuratowski embedding equals dist(a,x_n) − dist(x_0,x_n).

Русский

n-й координате встраивания Куротковского соответствует dist(a,x_n) − dist(x_0,x_n).

LaTeX

$$$\big(\mathrm{embeddingOfSubset}(x,a)\big)_n = \operatorname{dist}(a,x_n) - \operatorname{dist}(x_0,x_n)$$$

Lean4

theorem embeddingOfSubset_coe : embeddingOfSubset x a n = dist a (x n) - dist (x 0) (x n) :=
  rfl

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

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

Разделы

Аффилиация

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