English
For a fixed partition μ and an equivalence e: σ ≃ τ, there is an equivalence between the subtypes {x ∈ Sym σ n | ofSym x = μ} and {x ∈ Sym τ n | ofSym x = μ}.
Русский
Для фиксированного разбиения μ и эквивалентности e: σ ≃ τ существует эквивалентность между подтипами {x ∈ Sym σ n | ofSym x = μ} и {x ∈ Sym τ n | ofSym x = μ}.
LaTeX
$$$\mathrm{ofSymShapeEquiv}(\mu)(e) : \{x:Sym\,σ\,n\mid\mathrm{ofSym}(x)=\mu\} \simeq \{x:Sym\,τ\,n\mid\mathrm{ofSym}(x)=\mu\}$$$
Lean4
/-- An equivalence between `σ` and `τ` induces an equivalence between the subtypes of `Sym σ n` and
`Sym τ n` corresponding to a given partition. -/
def ofSymShapeEquiv (μ : Partition n) (e : σ ≃ τ) : { x : Sym σ n // ofSym x = μ } ≃ { x : Sym τ n // ofSym x = μ }
where
toFun := fun x => ⟨Sym.equivCongr e x, by simp [ofSym_map, x.2]⟩
invFun := fun x => ⟨Sym.equivCongr e.symm x, by simp [ofSym_map, x.2]⟩
left_inv := by intro x; simp
right_inv := by intro x; simp
