inl

Mathlib.Topology.Algebra.Module.LinearMapPiProd

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.inl

English

The left injection into a product is a continuous linear map.

Русский

Левое вложение в произведение — непрерывное линейное отображение.

LaTeX

$$$\text{inl}: M_1 \to_L[R] M_1 \times M_2$$$

Lean4

/-- The left injection into a product is a continuous linear map. -/
def inl : M₁ →L[R] M₁ × M₂ :=
  (ContinuousLinearMap.id R M₁).prod 0

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

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

Разделы

Аффилиация

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