subtypePerm_of_support_le — Mathlib

English

For a permutation c and a subset s with s containing the support of c, restricting c to s defines a permutation on s.

Русский

Для перестановки c и множества s, содержащеего опору c, ограничение c на s задаёт перестановку на s.

LaTeX

$$$c_{|s} \\in \\text{Perm}(s) \\quad \\text{whenever} \\quad \\operatorname{supp}(c) \\subseteq s$$$

Lean4

/-- Restrict a permutation to a Finset containing its support -/
def subtypePerm_of_support_le (c : Perm α) {s : Finset α} (hcs : c.support ⊆ s) : Equiv.Perm s :=
  subtypePerm c (isInvariant_of_support_le hcs)

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