cast_max — Mathlib

English

Let p, q ∈ ℚ and K be an ordered field in which the usual embedding ℚ → K exists. Then the image of max(p, q) in K equals the maximum of the images of p and q in K: (↑(max p q) : K) = max (p : K) (q : K).

Русский

Пусть p, q ∈ ℚ и K — упорядоченное поле с обычным включением ℚ в K. Тогда образ max(p, q) в K равен max образов p и q: (↑(max p q) : K) = max (p : K) (q : K).

LaTeX

$$$(\max(p,q))^K = \max(p^K,q^K)$$$

Lean4

@[simp, norm_cast]
theorem cast_max (p q : ℚ) : (↑(max p q) : K) = max (p : K) (q : K) :=
  (@cast_mono K _).map_max

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