symm_bijective

Mathlib.Algebra.Group.Action.Equidecomp

URI: https://scilib.ai/kg/mathlib#Equidecomp.symm_bijective

English

The symmetry map on equidecompositions is a bijection.

Русский

Отображение симметрии на эквидекомпозициях является биекцией.

LaTeX

$$$\\mathrm{symm}: \\mathrm{Equidecomp}(X,G) \\to \\mathrm{Equidecomp}(X,G)$ is bijective.$$

Lean4

theorem symm_bijective : Function.Bijective (symm : Equidecomp X G → _) :=
  symm_involutive.bijective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru