imCLM_norm

Mathlib.Analysis.Complex.OperatorNorm

URI: https://scilib.ai/kg/mathlib#Complex.imCLM_norm

← MathLib Explorer

English

The operator norm of the imaginary-part extraction map on ℂ is 1.

Русский

Норма оператора отображения мнимой части равна 1.

LaTeX

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

Lean4

@[simp]
theorem imCLM_norm : ‖imCLM‖ = 1 :=
  le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _) <|
    calc
      1 = ‖imCLM I‖ := by simp
      _ ≤ ‖imCLM‖ := unit_le_opNorm _ _ (by simp)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru