permCongr_apply

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.permCongr_apply

English

For p ∈ Perm α' and x in α', the action is (e.permCongr p)(x) = e(p(e^{-1}(x))).

Русский

Для p ∈ Perm α' и x ∈ α' выполняется (e.permCongr p)(x) = e(p(e^{-1}(x))).

LaTeX

$$$(e\text{.permCongr } p)(x) = e\bigl(p\bigl(e^{-1}(x)\bigr)\bigr)$$$

Lean4

@[simp, grind =]
theorem permCongr_apply (p : Equiv.Perm α') (x) : e.permCongr p x = e (p (e.symm x)) :=
  rfl

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

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

Разделы

Аффилиация

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