toPartialEquiv_restr — Mathlib

English

Restricting an equidecomposition to A commutes with converting to a partial equivalence: (f.restr A).toPartialEquiv = f.toPartialEquiv.restr A.

Русский

Ограничение эквидекомпозиции до A коммутирует с переходом к частичному эквив: (f.restr A).toPartialEquiv = f.toPartialEquiv.restr A.

LaTeX

$$$[\text{simp}]\; (f.restr A).toPartialEquiv = f.toPartialEquiv.restr A.$$$

Lean4

@[simp]
theorem toPartialEquiv_restr (f : Equidecomp X G) (A : Set X) : (f.restr A).toPartialEquiv = f.toPartialEquiv.restr A :=
  rfl

Похожие утверждения