le_map_mul_map_div — Mathlib

English

For any f in a suitable FunLike class and elements a,b in a group, 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) \cdot f\left(\frac{a}{b}\right)$$$

Lean4

@[to_additive]
theorem le_map_mul_map_div [Group α] [CommMagma β] [LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b : α) :
    f a ≤ f b * f (a / b) := by simpa only [mul_comm, div_mul_cancel] using map_mul_le_mul f (a / b) b

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