English
An index-set equivalence e: ι ≃ ι' induces a canonical equivalence between the spaces of continuous multilinear maps with indices ι and ι'.
Русский
Эквивалентность индексов e: ι ≃ ι' порождает естественное соответствие между пространствами непрерывных мультилинейных отображений с индексами ι и ι'.
LaTeX
$$Nonrec def domDomCongr {ι' : Type*} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun _ : ι => M₂) M₃) : ContinuousMultilinearMap R (fun _ : ι' => M₂) M₃$$
Lean4
@[ext]
theorem prod_ext {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)}
(h₁ :
(ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
(ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g)
(h₂ :
(ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
(ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g) :
f = g :=
prod_ext_iff.mpr ⟨h₁, h₂⟩
