English
Given a function f: α → ι, composition on product types yields a continuous linear map that precomposes by f. Concretely, it sends a family (v_i) indexed by ι to the family (v_{f(a)}) indexed by α.
Русский
Для функции f: α → ι композиция на продуктах задаёт непрерывный линейный отображение, которое по семейству (v_i) из индекса ι отправляет на семью (v_{f(a)}) по индексу α.
LaTeX
$$$$ (\Pi^{\phantom{}}\mathrm{compRightL}\; f)\; v\; a = v(f(a)) $$$$
Lean4
/-- Given a function `f : α → ι`, it induces a continuous linear function by right composition on
product types. For `f = Subtype.val`, this corresponds to forgetting some set of variables. -/
def _root_.Pi.compRightL {α : Type*} (f : α → ι) : ((i : ι) → φ i) →L[R] ((i : α) → φ (f i))
where
toFun := fun v i ↦ v (f i)
map_add' := by intros; ext; simp
map_smul' := by intros; ext; simp
cont := by fun_prop
