extendDomain_refl — Mathlib

English

Extending the identity permutation on α with domain f yields the identity permutation on β.

Русский

Расширение тождественной перестановки на α до β по f дает тождественную перестановку на β.

LaTeX

$$$\\mathrm{extendDomain}(\\mathrm{Equiv.refl}\\; α')\, f = \\mathrm{Equiv.refl}\\; β'$$$

Lean4

@[simp]
theorem extendDomain_refl : Perm.extendDomain (Equiv.refl _) f = Equiv.refl _ := by simp [Perm.extendDomain]

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