le_map_div_add_map_div — Mathlib

English

In the additive-male context, for suitable f and a,b,c, we have f(a/c) ≤ f(a/b) + f(b/c).

Русский

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

LaTeX

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

Lean4

@[to_additive existing]
theorem le_map_div_add_map_div [Group α] [Add β] [LE β] [MulLEAddHomClass F α β] (f : F) (a b c : α) :
    f (a / c) ≤ f (a / b) + f (b / c) := by simpa only [div_mul_div_cancel] using map_mul_le_add f (a / b) (b / c)

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