restr_univ

Mathlib.Algebra.Group.Action.Equidecomp

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

English

Restricting to the universal set leaves the equidecomposition unchanged: f.restr univ = f.

Русский

Ограничение до вселенного множества не меняет эквидекомпозицию: f.restr univ = f.

LaTeX

$$$\forall f:\mathrm{Equidecomp}(X,G), f.restr(\mathrm{univ}) = f.$$$

Lean4

@[simp]
theorem restr_univ (f : Equidecomp X G) : f.restr univ = f :=
  restr_of_source_subset <| subset_univ _

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

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

Разделы

Аффилиация

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