min_val — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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