min_mul_max — Mathlib

English

Let α be linearly ordered and β a commutative semigroup. Then for all a, b ∈ α, min(a, b) · max(a, b) = a · b.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem min_mul_max (a b : α) : min a b * max a b = a * b :=
  fn_min_mul_fn_max id _ _

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