norm_normedMk_eq_one — Mathlib

English

If there exists x with ‖x‖ ≠ 0, then the operator norm of normedMk is exactly 1.

Русский

Если существует x с ‖x‖ ≠ 0, то операционная норма normedMk равна единице.

LaTeX

$$$ \\| \\mathrm{normedMk} \\| = 1 \\quad\\text{if } \\exists x:\\, M, \\|x\\| \\neq 0$$$

Lean4

/-- The operator norm of the projection is `1` if there is an element whose norm is different from
`0`. -/
theorem norm_normedMk_eq_one (h : ∃ x : M, ‖x‖ ≠ 0) : ‖normedMk (M := M)‖ = 1 :=
  by
  apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one
  · simpa only [normedMk_apply, one_mul] using fun _ ↦ le_rfl
  · intro N _ hle
    obtain ⟨x, _⟩ := h
    exact one_le_of_le_mul_right₀ (by positivity) (hle x)

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