apply_abs_le_mul_of_one_le — Mathlib

English

If f: G → H is order-preserving with 1 ≤ f x for all x, then f(|a|) ≤ f(a) f(-a) for any a.

Русский

Если f: G → H сохраняет порядок и 1 ≤ f x для всех x, то f(|a|) ≤ f(a) f(-a).

LaTeX

$$\forall f:\ G \to H, \quad (\forall x, 1 \le f(x)) \Rightarrow f(|a|) \le f(a) f(-a)$$

Lean4

@[to_additive]
theorem apply_abs_le_mul_of_one_le {H : Type*} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H}
    (h : ∀ x, 1 ≤ f x) (a : G) : f |a| ≤ f a * f (-a) :=
  apply_abs_le_mul_of_one_le' (h _) (h _)

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