cast_min — Mathlib

English

For m,n ∈ ℕ, the cast of min(m,n) equals the minimum of the casts: (min(m,n) : α) = min(m:α, n:α).

Русский

Для m,n ∈ ℕ отображение min(m,n) в α равно минимуму m и n в α: (min(m,n) : α) = min(m:α, n:α).

LaTeX

$$$(\min(m,n) : \alpha) = \min(m : \alpha, n : \alpha)$$$

Lean4

@[simp, norm_cast]
theorem cast_min {α} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) :
    (↑(min m n : ℕ) : α) = min (m : α) n :=
  (@mono_cast α _).map_min

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