ball_zero_eq_Ico'

Mathlib.Topology.MetricSpace.Pseudo.Constructions

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

English

In NNReal, nndist(a,b) equals the max of (a-b) and (b-a).

Русский

nndist(a,b) = max(a-b, b-a).

LaTeX

$$$\\operatorname{nndist} a b = \\max(a - b, b - a)$$$

Lean4

theorem ball_zero_eq_Ico' (c : ℝ≥0) : Metric.ball (0 : ℝ≥0) c.toReal = Set.Ico 0 c := by ext x; simp

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

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

Разделы

Аффилиация

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