injOn_natAbs_Ici

Mathlib.Data.Int.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.injOn_natAbs_Ici

English

If a and b are nonnegative, then equality of their absolute values implies equality of the numbers themselves.

Русский

Если a и b неотрицательны, то |a| = |b| ⇒ a = b.

LaTeX

$$$\forall a,b \ge 0:\ |a| = |b| \Rightarrow a=b$$$

Lean4

theorem injOn_natAbs_Ici : InjOn natAbs (Ici 0) :=
  strictMonoOn_natAbs.injOn

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

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

Разделы

Аффилиация

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