English
Restriction of an equidecomposition to a set A yields a new equidecomposition on A, formed from the restriction of its partial equivalence and a restricted witness.
Русский
Ограничение эквидекомпозиции до множества A даёт новую эквидекомпозицию на A, состоящую из ограниченного частичного эквив и ограниченного свидетеля.
LaTeX
$$$\text{restr}(f,A) : \mathrm{Equidecomp}(X,G), \; \text{toPartialEquiv} := f.toPartialEquiv.restr A, \; \text{isDecompOn'} := \langle f.witness, f.isDecompOn.mono (\text{source_restr subset}) (\text{congrFun rfl}) \rangle.$$$
Lean4
/-- The restriction of an equidecomposition as an equidecomposition. -/
@[simps!]
def restr (f : Equidecomp X G) (A : Set X) : Equidecomp X G
where
toPartialEquiv := f.toPartialEquiv.restr A
isDecompOn' := ⟨f.witness, f.isDecompOn.mono (source_restr_subset_source _ _) fun _ ↦ congrFun rfl⟩
