instMonoid

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.instMonoid

English

The map p.subtypeₗᵢ is a linear isometry from p (as a space) to E.

Русский

Карта subtypeₗᵢ является линейной изометрией от p (как пространства) к E.

LaTeX

$$coe_subtypeₗᵢ : ⇑p.subtypeₗᵢ = p.subtype$$

Lean4

instance instMonoid : Monoid (E →ₗᵢ[R] E) where
  one := id
  mul := comp
  mul_assoc := comp_assoc
  one_mul := id_comp
  mul_one := comp_id

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

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

Разделы

Аффилиация

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