restr_refl_symm — Mathlib

English

Restricting the identity equidecomposition to a subset and then applying symmetry returns the same restricted equidecomposition.

Русский

Ограничение идентичной эквидекомпозиции до подмножества и последующее применение симметрии возвращают ту же ограниченную эквидекомпозицию.

LaTeX

$$$\\text{restr}(\\mathrm{refl}(X,G),A)^{\\mathrm{symm}} = \\text{restr}(\\mathrm{refl}(X,G),A).$$$

Lean4

@[simp]
theorem restr_refl_symm (A : Set X) : ((Equidecomp.refl X G).restr A).symm = (Equidecomp.refl X G).restr A :=
  rfl

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