English
There is a canonical bijection between Sym(Option α) n+1 and the disjoint sum Sym(Option α) n ⊕ Sym α n+1, given by encoding and decoding, with both compositions yielding the identity.
Русский
Существует каноническая биекция между Sym(Option α) n+1 и дизъюнктным суммой Sym(Option α) n ⊕ Sym α n+1, задаваемая кодированием и декодированием, для которой композиции дают тождество.
LaTeX
$$$\text{symOptionSuccEquiv} : \mathrm{Sym}(\mathrm{Option}\,\alpha)\,n.succ \simeq \mathrm{Sym}(\mathrm{Option}\,\alpha)\,n \oplus \mathrm{Sym}\,\alpha\,n.succ$$$
Lean4
/-- The symmetric product over `Option` is a disjoint union over simpler symmetric products. -/
--@[simps]
def symOptionSuccEquiv [DecidableEq α] : Sym (Option α) n.succ ≃ Sym (Option α) n ⊕ Sym α n.succ
where
toFun := SymOptionSuccEquiv.encode
invFun := SymOptionSuccEquiv.decode
left_inv := SymOptionSuccEquiv.decode_encode
right_inv := SymOptionSuccEquiv.encode_decode
