support_subtypePerm — Mathlib

English

The support of the restricted permutation f.subtypePerm h equals the set {x ∈ s | f x ≠ x}.

Русский

Опора ограниченной перестановки f.subtypePerm h равна множеству {x ∈ s | f x ≠ x}.

LaTeX

$$(f.subtypePerm h).\operatorname{support} = \{x \in s \mid f x \neq x\}$$

Lean4

@[simp]
theorem support_subtypePerm [DecidableEq α] {s : Finset α} (f : Perm α) (h) :
    (f.subtypePerm h : Perm s).support = ({x | f x ≠ x} : Finset s) := by ext; simp [Subtype.ext_iff]

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