reCLM_norm

Mathlib.Analysis.Complex.OperatorNorm

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

← MathLib Explorer

English

The real-part continuous linear map has operator norm 1.

Русский

Линейное отображение действительной части имеет норму оператора 1.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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