conjCLE_norm

Mathlib.Analysis.RCLike.Lemmas

URI: https://scilib.ai/kg/mathlib#RCLike.conjCLE_norm

English

The operator norm of conjCLE (the conjugation linear isometry) equals 1.

Русский

Нормa операторной конъюгированной линейной изометрии conjCLE равна 1.

LaTeX

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

Lean4

@[simp, rclike_simps]
theorem conjCLE_norm : ‖(@conjCLE K _ : K →L[ℝ] K)‖ = 1 :=
  (@conjLIE K _).toLinearIsometry.norm_toContinuousLinearMap

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

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

Разделы

Аффилиация

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