English
There is a continuous linear equivalence between the product M0 × Π i, M(Fin.succ i) and the full dependent product Π i, M i, which encodes inserting a head element in front of a sequence.
Русский
Существует непрерывно-линейное эквивалентное отображение между произведением M0 × Π i, M(Fin.succ i) и полным зависимым произведением Π i, M i, которое кодирует вставку головы в начало последовательности.
LaTeX
$$$ \text{Fin.consEquivL} : (M_0 \times \prod_{i:\, Fin n} M_{i.succ}) \simeq_L[R] \prod_{i:\, Fin n.succ} M_i, \\text{ с }\text{toFun}(a_0,(a_i)) (0)=a_0,\; \text{toFun}(a_0,(a_i))(\mathrm{Fin.succ}\ i)=a_i $$$
Lean4
/-- `Fin.consEquiv` as a continuous linear equivalence. -/
@[simps!]
def _root_.Fin.consEquivL : (M 0 × Π i, M (Fin.succ i)) ≃L[R] (Π i, M i)
where
__ := Fin.consLinearEquiv R M
continuous_toFun := continuous_id.fst.finCons continuous_id.snd
continuous_invFun := .prodMk (continuous_apply 0) (by continuity)
