apply_abs_le_mul_of_one_le' — Mathlib

English

Let f: G → H with H a Monoid, and f is order-preserving on multiplication from both sides. If 1 ≤ f(a) and 1 ≤ f(-a), then f(|a|) ≤ f(a) f(-a).

Русский

Пусть f: G → H сохраняет порядок умножения, и 1 ≤ f(a), 1 ≤ f(-a). Тогда f(|a|) ≤ f(a) f(-a).

LaTeX

$$\forall f:\ G \to H, \quad 1 \le f(a) \land 1 \le f(-a) \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}
    {a : G} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a) :=
  (le_total a 0).rec (fun ha => (abs_of_nonpos ha).symm ▸ le_mul_of_one_le_left' h₁) fun ha =>
    (abs_of_nonneg ha).symm ▸ le_mul_of_one_le_right' h₂

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