map_one_le_one — Mathlib

English

If f is power-multiplicative, then f(1) ≤ 1.

Русский

Если f является функцией с свойством степенного умножения, то f(1) ≤ 1.

LaTeX

$$$\forall f:\,R\to\mathbb{R},\ hf:\mathrm{IsPowMul}(f) \Rightarrow f(1) \le 1$$$

Lean4

theorem map_one_le_one {R : Type*} [Monoid R] {f : R → ℝ} (hf : IsPowMul f) : f 1 ≤ 1 :=
  by
  have hf1 : (f 1) ^ 2 = f 1 := by conv_rhs => rw [← one_pow 2, hf _ one_le_two]
  rcases eq_zero_or_one_of_sq_eq_self hf1 with h | h <;> rw [h]
  exact zero_le_one

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