le_map_add_map_div — Mathlib

English

In the additive setting, for suitable f and a,b, we have f(a) ≤ f(b) + f(a/b).

Русский

В аддитивной настройке для подходящих f и a, b выполняется f(a) ≤ f(b) + f(a/b).

LaTeX

$$$f(a) \le f(b) + f\left(\frac{a}{b}\right)$$$

Lean4

@[to_additive existing]
theorem le_map_add_map_div [Group α] [AddCommMagma β] [LE β] [MulLEAddHomClass F α β] (f : F) (a b : α) :
    f a ≤ f b + f (a / b) := by simpa only [add_comm, div_mul_cancel] using map_mul_le_add f (a / b) b

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