English
Let f be an equidecomposition on X with group G. Then f is decomposable on its source f.source via a witness set f.witness, i.e., IsDecompOn f f.source f.witness.
Русский
Пусть f — эквидекомпозиция на X с группой G. Тогда f раскладываема на источнике f.source с опорой на множество свидетелей f.witness, то есть IsDecompOn f f.source f.witness.
LaTeX
$$$\text{IsDecompOn} \ f \ f.source \ f.witness.$$$
Lean4
/-- Let `G` act on a space `X` and `A : Set X`. We say `f : X → X` is a decomposition on `A`
as witnessed by some `S : Finset G` if for all `a ∈ A`, the value `f a` can be obtained
by applying some element of `S` to `a` instead.
More familiarly, the restriction of `f` to `A` is the result of partitioning `A` into finitely many
pieces, then applying a single element of `G` to each piece. -/
def IsDecompOn (f : X → X) (A : Set X) (S : Finset G) : Prop :=
∀ a ∈ A, ∃ g ∈ S, f a = g • a
