norm_fst — Mathlib

English

The operator norm of the first projection fst is exactly 1 when E is nontrivial.

Русский

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

LaTeX

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

Lean4

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

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