derangements.Equiv.RemoveNone.fiber_some

theorem derangements.Equiv.RemoveNone.fiber_some : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), derangements.Equiv.RemoveNone.fiber (some a) = {f | Function.fixedPoints ⇑f ⊆ {a}}

The theorem `derangements.Equiv.RemoveNone.fiber_some` states that for any type `α` with decidable equality and any element `a` of this type, the fiber over `some a` in the context of derangements is the set of permutations where `a` is the only possible fixed point. In other words, the set of permutations that when decomposed, result in `a` as the only derangement, is equal to the set of permutations where the fixed points of the permutation are a subset of the set containing `a` only.

More concisely: The theorem asserts that the fiber of the derangement equivalence relation over some element `a` in type `α` consists of permutations that fix exactly `a` and no other elements.