dist_self

Mathlib.Topology.MetricSpace.PiNat

URI: https://scilib.ai/kg/mathlib#PiNat.dist_self

English

For any index family of spaces E_n, the distance from any element to itself is zero.

Русский

Для любой системы пространств E_n расстояние между элементом и самим собой равно нулю.

LaTeX

$$$$ \forall x,\; \operatorname{dist}(x,x)=0 $$$$

Lean4

protected theorem dist_self (x : ∀ n, E n) : dist x x = 0 := by simp [dist]

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

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

Разделы

Аффилиация

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