English
If the norm on K is nonarchimedean, then B.norm is nonarchimedean on L.
Русский
Если норма на K является нерarchимедовой, то норма B на L тоже неархимедова.
LaTeX
$$IsNonarchimedean(B.norm)$$
Lean4
/-- For any `K`-basis of `L`, if the norm on `K` is nonarchimedean, then so is `B.norm`. -/
theorem norm_isNonarchimedean (hna : IsNonarchimedean (Norm.norm : K → ℝ)) : IsNonarchimedean B.norm := fun x y ↦
by
obtain ⟨ixy, _, hixy⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖(B.repr (x + y)) i‖)
have hxy : ‖B.repr (x + y) ixy‖ ≤ max ‖B.repr x ixy‖ ‖B.repr y ixy‖ := by
rw [LinearEquiv.map_add, Finsupp.coe_add, Pi.add_apply]; exact hna _ _
rw [Basis.norm, hixy]
rcases le_max_iff.mp hxy with (hx | hy)
· exact le_max_of_le_left (le_trans hx (norm_repr_le_norm B ixy))
· exact le_max_of_le_right (le_trans hy (norm_repr_le_norm B ixy))
