norm_subtypeL

Mathlib.Analysis.Normed.Operator.NormedSpace

URI: https://scilib.ai/kg/mathlib#Submodule.norm_subtypeL

English

For any nontrivial subspace K, the operator norm of its subtype map equals 1.

Русский

Для любого ненулевого подпространства K операторная норма подтипового отображения равна 1.

LaTeX

$$$\\|K.subtypeL\\| = 1$ for [Nontrivial K].$$

Lean4

theorem norm_subtypeL (K : Submodule 𝕜 E) [Nontrivial K] : ‖K.subtypeL‖ = 1 :=
  K.subtypeₗᵢ.norm_toContinuousLinearMap

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

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

Разделы

Аффилиация

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