le_map_tsub — Mathlib

English

If f preserves addition on α and b ≤ a, then f(a − b) = f(a) − f(b).

Русский

Если f сохраняет сложение на α и b ≤ a, то f(a − b) = f(a) − f(b).

LaTeX

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

Lean4

theorem le_map_tsub [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β) (hf : Monotone f) (a b : α) :
    f a - f b ≤ f (a - b) := by
  rw [tsub_le_iff_right, ← f.map_add]
  exact hf le_tsub_add

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