English
Let X be a set with a G-action. The identity map on X provides an equidecomposition of X with itself; in particular, X decomposes into a single piece corresponding to the identity element of G.
Русский
Пусть X — множество, на котором действует моноид G. Единичное отображение на X дает эквидекомпозицию X самой по себе; в частности, X распадается на одну часть, соответствующую единице в G.
LaTeX
$$$\\exists e \\in \\mathrm{Equidecomp}(X,G)\\;\\text{ such that }\\; e\\text{ encodes the identity on }X.$$$
Lean4
/-- The identity function is an equidecomposition of the space with itself. -/
@[simps toPartialEquiv]
def refl : Equidecomp X G where
toPartialEquiv := .refl _
isDecompOn' := ⟨{ 1 }, by simp [IsDecompOn]⟩
