English
Equivalences of index sets yield canonical equivalences between spaces of continuous multilinear maps, reindexed accordingly.
Русский
Эквивалентности множеств индексов порождают канонические эквивалентности между пространствами непрерывных мультиленейных отображений с перенастройкой индексов.
LaTeX
$$Nonrec def domDomCongr {ι' : Type*} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun _ : ι => M₂) M₃) : ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃$$
Lean4
/-- An equivalence of the index set defines an equivalence between the spaces of continuous
multilinear maps. This is the forward map of this equivalence. -/
@[simps! toMultilinearMap apply]
nonrec def domDomCongr {ι' : Type*} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun _ : ι => M₂) M₃) :
ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃
where
toMultilinearMap := f.domDomCongr e
cont := f.cont.comp <| continuous_pi fun _ => continuous_apply _
