le_map_tsub

Mathlib.Algebra.Order.Sub.Unbundled.Hom

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.le_map_tsub

← MathLib Explorer

English

If c ≤ a, then a + b − (a − c) = b + c.

Русский

Если c ≤ a, то a + b − (a − c) = b + c.

LaTeX

$$$\forall a,b,c \in \alpha\,(c \le a) \Rightarrow a + b - (a - c) = b + c$$$

Lean4

theorem le_map_tsub [Preorder β] [AddZeroClass β] [Sub β] [OrderedSub β] (f : α →+ β) (hf : Monotone f) (a b : α) :
    f a - f b ≤ f (a - b) :=
  f.toAddHom.le_map_tsub hf a b

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

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

Разделы

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

Аффилиация

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