dist_eq_of_ne

Mathlib.Topology.MetricSpace.PiNat

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

English

If x ≠ y, then dist x y = (1/2)^{firstDiff x y}.

Русский

Если x ≠ y, то dist(x,y) = (1/2)^{firstDiff(x,y)}.

LaTeX

$$$x \\neq y \\Rightarrow \\operatorname{dist}(x,y)=(1/2)^{\\mathrm{firstDiff}(x,y)}$$$

Lean4

theorem dist_eq_of_ne {x y : ∀ n, E n} (h : x ≠ y) : dist x y = (1 / 2 : ℝ) ^ firstDiff x y := by simp [dist, h]

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

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

Разделы

Аффилиация

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