norm_extends — Mathlib

English

If B is a K-basis of L containing 1, then B.norm extends the norm on K; i.e. B.norm(algebraMap_K_L x) = ||x|| for all x in K.

Русский

Если B — базис L над K, содержащий 1, тогда B.norm распространяет норму на K: для всех x ∈ K выполняется B.norm(algebraMap_K_L x) = ||x||.

LaTeX

$$$\forall x \in K,\ B.norm((\mathrm{algebraMap} \\ K \\ L) x) = \|x\|$$$

Lean4

/-- For any `K`-basis `B` of `L` containing `1`, `B.norm` extends the norm on `K`. -/
theorem norm_extends {i : ι} (hBi : B i = (1 : L)) (x : K) : B.norm ((algebraMap K L) x) = ‖x‖ := by
  classical
  simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)

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