map_sub_eq_zero_iff

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.map_sub_eq_zero_iff

← MathLib Explorer

English

abv(a - b) = 0 iff a = b.

Русский

abv(a-b)=0 тогда и только тогда a=b.

LaTeX

$$$abv(a-b)=0\iff a=b$$$

Lean4

@[simp high] -- added `high` to apply it before `AbsoluteValue.eq_zero`

theorem map_sub_eq_zero_iff (a b : R) : abv (a - b) = 0 ↔ a = b :=
  abv.eq_zero.trans sub_eq_zero

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

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

Разделы

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

Аффилиация

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