le_add_nndist

Mathlib.Topology.MetricSpace.Pseudo.Constructions

URI: https://scilib.ai/kg/mathlib#NNReal.le_add_nndist

← MathLib Explorer

English

For a,b in NNReal, a ≤ b + nndist(a,b).

Русский

Для a,b ∈ NNReal выполнено a ≤ b + nndist(a,b).

LaTeX

$$$a \\le b + \\operatorname{nndist}(a,b)$$$

Lean4

theorem le_add_nndist (a b : ℝ≥0) : a ≤ b + nndist a b :=
  by
  suffices (a : ℝ) ≤ (b : ℝ) + dist a b by rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
  rw [← sub_le_iff_le_add']
  exact le_of_abs_le (dist_eq a b).ge

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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