opNorm_zero_iff — Mathlib

English

A continuous multilinear map has operator norm zero if and only if the map itself is the zero map.

Русский

Операторная норма непрерывного многолинейного отображения равна нулю тогда и только тогда, когда отображение равно нулю.

LaTeX

$$$\|f\| = 0 \ \Longleftrightarrow\ f = 0$$$

Lean4

/-- A continuous linear map is zero iff its norm vanishes. -/
theorem opNorm_zero_iff {f : ContinuousMultilinearMap 𝕜 E G} : ‖f‖ = 0 ↔ f = 0 := by
  simp [← (opNorm_nonneg f).ge_iff_eq', opNorm_le_iff le_rfl, ContinuousMultilinearMap.ext_iff]

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