norm_snd — Mathlib

English

The operator norm of the second projection snd is exactly 1 when F is nontrivial.

Русский

Норма оператора второй проекции snd равна единице, если F не тривиально.

LaTeX

$$$$\\|\\mathrm{snd}\\| = 1.$$$$

Lean4

/-- The operator norm of the second projection `E × F → F` is exactly 1 if `F` is nontrivial. -/
@[simp]
theorem norm_snd [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial F] :
    ‖snd 𝕜 E F‖ = 1 := by
  refine le_antisymm (norm_snd_le ..) ?_
  let ⟨f, hf⟩ := exists_ne (0 : F)
  have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f)
  rw [norm_zero, max_eq_right (norm_nonneg f)] at this
  rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul]

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