English
The combination of two equidecompositions yields a new equidecomposition; the operation is closed on Equidecomp X G.
Русский
Комбинация двух эквидекомпозиций даёт новую эквидекомпозицию; операция замкнута в пространстве Equidecomp X G.
LaTeX
$$$f,g \\in \\mathrm{Equidecomp}(X,G) \\Rightarrow f \\mathrm{.trans} g \\in \\mathrm{Equidecomp}(X,G).$$$
Lean4
/-- The composition of two equidecompositions as an equidecomposition. -/
@[simps toPartialEquiv, trans]
noncomputable def trans (f g : Equidecomp X G) : Equidecomp X G
where
toPartialEquiv := f.toPartialEquiv.trans g.toPartialEquiv
isDecompOn' := by classical exact ⟨g.witness * f.witness, g.isDecompOn.comp' f.isDecompOn⟩
