nndist_eq

Mathlib.Topology.Instances.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.nndist_eq

English

nndist on ℚ≥0 coincides with nndist on ℚ after casting.

Русский

nndist на ℚ≥0 совпадает с nndist на ℚ после приведения.

LaTeX

$$$\\operatorname{nndist}_{\\mathbb{Q}_{\\ge 0}}(p,q) = \\operatorname{nndist}_{\\mathbb{Q}}(p,q).$$$

Lean4

@[simp← , push_cast]
theorem nndist_eq (p q : ℚ≥0) : nndist p q = nndist (p : ℚ) (q : ℚ) :=
  rfl

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

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

Разделы

Аффилиация

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