tsub_left_inj

Mathlib.Algebra.Order.Sub.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#tsub_left_inj

← MathLib Explorer

English

If c ≤ a and c ≤ b, then a − c = b − c ⇔ a = b.

Русский

Если c ≤ a и c ≤ b, то a − c = b − c эквивалентно a = b.

LaTeX

$$$ c \\le a \\land c \\le b \\Rightarrow a - c = b - c \\iff a = b $$$

Lean4

theorem tsub_left_inj (h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b := by
  simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]

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

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

Разделы

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

Аффилиация

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