English
The map Pi.single i: φ_i →L[R] (∏_i φ_i) embeds the i-th coordinate by sending x in φ_i to the element in the product whose i-th component is x and all other components are zero; this is a bundled continuous linear map.
Русский
Отображение Pi.single i: φ_i →L[R] (∏_i φ_i) вставляет i-ю координату, отправляя x в φ_i в элемент произведения, у которого i-я компонента равна x, а остальные нули; это упакованное непрерывное линейное отображение.
LaTeX
$$$$ \text{Pi.single } i: \; φ_i \to_L[R] (\prod_i φ_i) \quad\text{with}\quad (\text{Pi.single } i)(x)(j) = \begin{cases} x & j = i, \\ 0 & j \neq i. \end{cases} $$$$
Lean4
/-- `Pi.single` as a bundled continuous linear map. -/
@[simps! -fullyApplied]
def single [DecidableEq ι] (i : ι) : φ i →L[R] (∀ i, φ i)
where
toLinearMap := .single R φ i
cont := continuous_single _
