fn_min_mul_fn_max — Mathlib

English

For any function f: α → β with β a commutative semigroup, f(min(a,b)) ⋅ f(max(a,b)) = f(a) ⋅ f(b).

Русский

Для любой функции f: α → β, β — коммутативная полугруппа, выполняется f(min(a,b))⋅f(max(a,b)) = f(a)⋅f(b).

LaTeX

$$$\forall f:\alpha\to\beta,\forall a,b:\alpha,\ f(\min(a,b)) \;*\; f(\max(a,b)) = f(a) \;*\; f(b).$$$

Lean4

@[to_additive]
theorem fn_min_mul_fn_max (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b := by
  obtain h | h := le_total a b <;> simp [h, mul_comm]

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