fn_max_mul_fn_min — Mathlib

English

Let α be a linearly ordered set and β a commutative semigroup. For every function f: α → β and any a, b ∈ α, the product f(max(a, b)) · f(min(a, b)) equals f(a) · f(b).

Русский

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

LaTeX

$$$ f(\\max(a,b)) \\cdot f(\\min(a,b)) = f(a) \\cdot f(b) $$$

Lean4

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

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