cast_max — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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