dist_eq

Mathlib.Topology.Instances.Rat

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

English

Distance in ℚ≥0 matches distance in ℚ after cast.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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