max_val — Mathlib

English

The value of the maximum of two units equals the maximum of their values: max a b .val = max(a.val, b.val).

Русский

Значение максимума двух единиц равно максимуму их значений: max a b .val = max(a.val, b.val).

LaTeX

$$$\\forall a,b \\in \\mathrm{Units}(\\alpha),\\ (\\mathrm{max}\\ a\\ b).\\mathrm{val} = \\max(a.\\mathrm{val}, b.\\mathrm{val})$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem max_val [Monoid α] [LinearOrder α] (a b : αˣ) : (max a b).val = max a.val b.val :=
  by
  simp_rw [max_def, val_le_val, ← apply_ite]
  rfl

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