English
Let a be an element of Option α and f a permutation of α. Then f lies in RemoveNone.fiber a if and only if there exists a permutation F of Option α that is a derangement with F(None) = a and removeNone F = f.
Русский
Пусть a ∈ Option α и f ∈ Perm α. Тогда f ∈ RemoveNone.fiber a тогда и только тогда, когда существует перестановка F на Option α, являющаяся перестановкой без фиксаций, такая что F None = a и removeNone F = f.
LaTeX
$$$ f \\in RemoveNone.fiber a \\iff \\exists F : Perm (Option \\alpha), F \\in derangements (Option \\alpha) \\land F\\,none = a \\land removeNone F = f $$$
Lean4
theorem mem_fiber (a : Option α) (f : Perm α) :
f ∈ RemoveNone.fiber a ↔ ∃ F : Perm (Option α), F ∈ derangements (Option α) ∧ F none = a ∧ removeNone F = f := by
simp [RemoveNone.fiber, derangements]
