nndist_zero_eq_val'

Mathlib.Topology.MetricSpace.Pseudo.Constructions

URI: https://scilib.ai/kg/mathlib#NNReal.nndist_zero_eq_val'

English

For z ∈ NNReal, nndist 0 z equals z.

Русский

Для z ∈ NNReal, nndist(0,z) равно z.

LaTeX

$$$\\operatorname{nndist}(0,z) = z$$$

Lean4

@[simp]
theorem nndist_zero_eq_val' (z : ℝ≥0) : nndist z 0 = z :=
  by
  rw [nndist_comm]
  exact NNReal.nndist_zero_eq_val z

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

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

Разделы

Аффилиация

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