reCLM_norm — Mathlib

English

The operator norm of the real-conjugate linear map reCLM on K is 1.

Русский

Нормa операторной нормой у реал-подстановки reCLM на K равна 1.

LaTeX

$$$\\|\\mathrm{reCLM}\\| = 1$$$

Lean4

@[simp, rclike_simps]
theorem reCLM_norm : ‖(reCLM : StrongDual ℝ K)‖ = 1 :=
  by
  apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)
  convert ContinuousLinearMap.ratio_le_opNorm (reCLM : StrongDual ℝ K) (1 : K)
  simp

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