le_map_div_mul_map_div — Mathlib

English

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

Lean4

@[to_additive]
theorem le_map_div_mul_map_div [Group α] [Mul β] [LE β] [SubmultiplicativeHomClass 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_mul f (a / b) (b / c)

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