English
There is a natural equivalence between families of continuous alternating maps indexed by a finite index set ι', and a single continuous alternating map whose domain is M and codomain is the family ∀ i, N i.
Русский
Существует естественное эквивалентность между семействами непрерывных чередующих карт, индексированных множеством ι', и одной картой с областью M и кодом ∀ i, N i.
LaTeX
$$$\text{Equiv}\left(\{i\mapsto \text{ContinuousAlternatingMap }R\;M\;N_i\;ι\},\;\text{ContinuousAlternatingMap }R\;M\;((i\mapsto N_i))\;ι\right).$$$
Lean4
/-- `ContinuousAlternatingMap.pi` as an `Equiv`. -/
@[simps]
def piEquiv {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, TopologicalSpace (N i)]
[∀ i, Module R (N i)] : (∀ i, M [⋀^ι]→L[R] N i) ≃ M [⋀^ι]→L[R] ∀ i, N i
where
toFun := pi
invFun f i := (ContinuousLinearMap.proj i : _ →L[R] N i).compContinuousAlternatingMap f
